This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zfpair

Description: The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of TakeutiZaring p. 15. In some textbooks this is stated as a separate axiom; here we show it is redundant since it can be derived from the other axioms.

This theorem should not be referenced by any proof other than axprALT . Instead, use zfpair2 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 18-Oct-1995) (New usage is discouraged.)

Ref Expression
Assertion zfpair ⊢ x y ∈ V

Proof

Step Hyp Ref Expression
1 dfpr2 ⊢ x y = w | w = x ∨ w = y
2 19.43 ⊢ ∃ z z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y ↔ ∃ z z = ∅ ∧ w = x ∨ ∃ z z = ∅ ∧ w = y
3 prlem2 ⊢ z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y ↔ z = ∅ ∨ z = ∅ ∧ z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y
4 3 exbii ⊢ ∃ z z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y ↔ ∃ z z = ∅ ∨ z = ∅ ∧ z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y
5 0ex ⊢ ∅ ∈ V
6 5 isseti ⊢ ∃ z z = ∅
7 19.41v ⊢ ∃ z z = ∅ ∧ w = x ↔ ∃ z z = ∅ ∧ w = x
8 6 7 mpbiran ⊢ ∃ z z = ∅ ∧ w = x ↔ w = x
9 p0ex ⊢ ∅ ∈ V
10 9 isseti ⊢ ∃ z z = ∅
11 19.41v ⊢ ∃ z z = ∅ ∧ w = y ↔ ∃ z z = ∅ ∧ w = y
12 10 11 mpbiran ⊢ ∃ z z = ∅ ∧ w = y ↔ w = y
13 8 12 orbi12i ⊢ ∃ z z = ∅ ∧ w = x ∨ ∃ z z = ∅ ∧ w = y ↔ w = x ∨ w = y
14 2 4 13 3bitr3ri ⊢ w = x ∨ w = y ↔ ∃ z z = ∅ ∨ z = ∅ ∧ z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y
15 14 abbii ⊢ w | w = x ∨ w = y = w | ∃ z z = ∅ ∨ z = ∅ ∧ z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y
16 dfpr2 ⊢ ∅ ∅ = z | z = ∅ ∨ z = ∅
17 pp0ex ⊢ ∅ ∅ ∈ V
18 16 17 eqeltrri ⊢ z | z = ∅ ∨ z = ∅ ∈ V
19 equequ2 ⊢ v = x → w = v ↔ w = x
20 0inp0 ⊢ z = ∅ → ¬ z = ∅
21 19 20 prlem1 ⊢ v = x → z = ∅ → z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y → w = v
22 21 alrimdv ⊢ v = x → z = ∅ → ∀ w z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y → w = v
23 22 spimevw ⊢ z = ∅ → ∃ v ∀ w z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y → w = v
24 orcom ⊢ z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y ↔ z = ∅ ∧ w = y ∨ z = ∅ ∧ w = x
25 equequ2 ⊢ v = y → w = v ↔ w = y
26 20 con2i ⊢ z = ∅ → ¬ z = ∅
27 25 26 prlem1 ⊢ v = y → z = ∅ → z = ∅ ∧ w = y ∨ z = ∅ ∧ w = x → w = v
28 24 27 syl7bi ⊢ v = y → z = ∅ → z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y → w = v
29 28 alrimdv ⊢ v = y → z = ∅ → ∀ w z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y → w = v
30 29 spimevw ⊢ z = ∅ → ∃ v ∀ w z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y → w = v
31 23 30 jaoi ⊢ z = ∅ ∨ z = ∅ → ∃ v ∀ w z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y → w = v
32 18 31 zfrep4 ⊢ w | ∃ z z = ∅ ∨ z = ∅ ∧ z = ∅ ∧ w = x ∨ z = ∅ ∧ w = y ∈ V
33 15 32 eqeltri ⊢ w | w = x ∨ w = y ∈ V
34 1 33 eqeltri ⊢ x y ∈ V