Metamath Proof Explorer

Theorem axpr

Description: Unabbreviated version of the Axiom of Pairing of ZF set theory, derived as a theorem from the other axioms.

This theorem should not be referenced by any proof. Instead, use ax-pr below so that the uses of the Axiom of Pairing can be more easily identified.

For a shorter proof using ax-ext , see axprALT . (Contributed by NM, 14-Nov-2006) Remove dependency on ax-ext . (Revised by Rohan Ridenour, 10-Aug-2023) (Proof shortened by BJ, 13-Aug-2023) Use ax-pr instead. (New usage is discouraged.)

Ref Expression
Assertion axpr ⊢∃z∀ww=x∨w=y→w∈z

Proof

Step Hyp Ref Expression
1 axprlem3 ⊢∃z∀ww∈z↔∃ss∈p∧if-∃nn∈sw=xw=y
2 biimpr ⊢w∈z↔∃ss∈p∧if-∃nn∈sw=xw=y→∃ss∈p∧if-∃nn∈sw=xw=y→w∈z
3 2 alimi ⊢∀ww∈z↔∃ss∈p∧if-∃nn∈sw=xw=y→∀w∃ss∈p∧if-∃nn∈sw=xw=y→w∈z
4 1 3 eximii ⊢∃z∀w∃ss∈p∧if-∃nn∈sw=xw=y→w∈z
5 axprlem4 ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=x→∃ss∈p∧if-∃nn∈sw=xw=y
6 axprlem5 ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=y→∃ss∈p∧if-∃nn∈sw=xw=y
7 5 6 jaodan ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=x∨w=y→∃ss∈p∧if-∃nn∈sw=xw=y
8 7 ex ⊢∀s∀n∈s∀t¬t∈n→s∈p→w=x∨w=y→∃ss∈p∧if-∃nn∈sw=xw=y
9 8 imim1d ⊢∀s∀n∈s∀t¬t∈n→s∈p→∃ss∈p∧if-∃nn∈sw=xw=y→w∈z→w=x∨w=y→w∈z
10 9 alimdv ⊢∀s∀n∈s∀t¬t∈n→s∈p→∀w∃ss∈p∧if-∃nn∈sw=xw=y→w∈z→∀ww=x∨w=y→w∈z
11 10 eximdv ⊢∀s∀n∈s∀t¬t∈n→s∈p→∃z∀w∃ss∈p∧if-∃nn∈sw=xw=y→w∈z→∃z∀ww=x∨w=y→w∈z
12 4 11 mpi ⊢∀s∀n∈s∀t¬t∈n→s∈p→∃z∀ww=x∨w=y→w∈z
13 axprlem2 ⊢∃p∀s∀n∈s∀t¬t∈n→s∈p
14 12 13 exlimiiv ⊢∃z∀ww=x∨w=y→w∈z