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

Metamath Proof Explorer

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