Metamath Proof Explorer

Theorem prexOLD

Description: Obsolete version of prex as of 6-Mar-2026. (Contributed by NM, 15-Jul-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion prexOLD 
|- { A , B } e. _V

Proof

Step Hyp Ref Expression
1 preq2 
 |-  ( y = B -> { x , y } = { x , B } )
2 1 eleq1d 
 |-  ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3 zfpair2 
 |-  { x , y } e. _V
4 2 3 vtoclg 
 |-  ( B e. _V -> { x , B } e. _V )
5 preq1 
 |-  ( x = A -> { x , B } = { A , B } )
6 5 eleq1d 
 |-  ( x = A -> ( { x , B } e. _V <-> { A , B } e. _V ) )
7 4 6 imbitrid 
 |-  ( x = A -> ( B e. _V -> { A , B } e. _V ) )
8 7 vtocleg 
 |-  ( A e. _V -> ( B e. _V -> { A , B } e. _V ) )
9 prprc1 
 |-  ( -. A e. _V -> { A , B } = { B } )
10 snexOLD 
 |-  { B } e. _V
11 9 10 eqeltrdi 
 |-  ( -. A e. _V -> { A , B } e. _V )
12 prprc2 
 |-  ( -. B e. _V -> { A , B } = { A } )
13 snexOLD 
 |-  { A } e. _V
14 12 13 eqeltrdi 
 |-  ( -. B e. _V -> { A , B } e. _V )
15 8 11 14 pm2.61nii 
 |-  { A , B } e. _V