prod_elimr

Theorem prod_elimr

Theorem. prod_elimr
t ∈ X × Y → scd t ∈ Y

Proof
01. 1 ⊢ t ∈ X × Y, hypo.
02. 1 ⊢ fst t ∈ X ∧ scd t ∈ Y, prod_elim_lemma 1.
03. 1 ⊢ scd t ∈ Y, conj_elimr 2.
prod_elimr. ⊢ t ∈ X × Y → scd t ∈ Y, subj_intro 3.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing.