Theorem prex

Description: The Axiom of Pairing using class variables. Theorem 7.13 of Quine p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc ), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993)

	Ref	Expression
Assertion	prex	⊢ { 𝐴 , 𝐵 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		preq2	⊢ ( 𝑦 = 𝐵 → { 𝑥 , 𝑦 } = { 𝑥 , 𝐵 } )
2	1	eleq1d	⊢ ( 𝑦 = 𝐵 → ( { 𝑥 , 𝑦 } ∈ V ↔ { 𝑥 , 𝐵 } ∈ V ) )
3		zfpair2	⊢ { 𝑥 , 𝑦 } ∈ V
4	2 3	vtoclg	⊢ ( 𝐵 ∈ V → { 𝑥 , 𝐵 } ∈ V )
5		preq1	⊢ ( 𝑥 = 𝐴 → { 𝑥 , 𝐵 } = { 𝐴 , 𝐵 } )
6	5	eleq1d	⊢ ( 𝑥 = 𝐴 → ( { 𝑥 , 𝐵 } ∈ V ↔ { 𝐴 , 𝐵 } ∈ V ) )
7	4 6	imbitrid	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∈ V → { 𝐴 , 𝐵 } ∈ V ) )
8	7	vtocleg	⊢ ( 𝐴 ∈ V → ( 𝐵 ∈ V → { 𝐴 , 𝐵 } ∈ V ) )
9		prprc1	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 , 𝐵 } = { 𝐵 } )
10		snex	⊢ { 𝐵 } ∈ V
11	9 10	eqeltrdi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 , 𝐵 } ∈ V )
12		prprc2	⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } = { 𝐴 } )
13		snex	⊢ { 𝐴 } ∈ V
14	12 13	eqeltrdi	⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } ∈ V )
15	8 11 14	pm2.61nii	⊢ { 𝐴 , 𝐵 } ∈ V