prod_eliml

Theorem prod_eliml

Theorem. prod_eliml
t ∈ X × Y → fst t ∈ X

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

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