# 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 syl5ib ( 𝑥 = 𝐴 → ( 𝐵 ∈ 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