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	⊢ { 𝑥 , 𝑦 } ∈ V

Proof

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