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 ∀ w w = x ∨ w = y → w ∈ z

Proof

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