MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prex Unicode version

Theorem prex 4189
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 3712), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
prex  |-  { A ,  B }  e.  _V

Proof of Theorem prex
StepHypRef Expression
1 preq2 3681 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2324 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4187 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 2818 . . . 4  |-  ( B  e.  _V  ->  { x ,  B }  e.  _V )
5 preq1 3680 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2324 . . . 4  |-  ( x  =  A  ->  ( { x ,  B }  e.  _V  <->  { A ,  B }  e.  _V ) )
74, 6syl5ib 212 . . 3  |-  ( x  =  A  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
87vtocleg 2829 . 2  |-  ( A  e.  _V  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
9 prprc1 3710 . . 3  |-  ( -.  A  e.  _V  ->  { A ,  B }  =  { B } )
10 snex 4188 . . 3  |-  { B }  e.  _V
119, 10syl6eqel 2346 . 2  |-  ( -.  A  e.  _V  ->  { A ,  B }  e.  _V )
12 prprc2 3711 . . 3  |-  ( -.  B  e.  _V  ->  { A ,  B }  =  { A } )
13 snex 4188 . . 3  |-  { A }  e.  _V
1412, 13syl6eqel 2346 . 2  |-  ( -.  B  e.  _V  ->  { A ,  B }  e.  _V )
158, 11, 14pm2.61nii 160 1  |-  { A ,  B }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    = wceq 1619    e. wcel 1621   _Vcvv 2763   {csn 3614   {cpr 3615
This theorem is referenced by:  opex  4209  opi2  4213  opth  4217  opeqsn  4234  opeqpr  4235  opthwiener  4240  uniop  4241  fr2nr  4343  unex  4490  tpex  4491  op1stb  4541  xpsspwOLD  4786  relop  4822  pw2f1olem  6934  1sdom  7033  opthreg  7287  pr2ne  7603  dfac2  7725  intwun  8325  wunex2  8328  wuncval2  8337  intgru  8404  xrex  10318  prmreclem2  12926  prdsval  13317  imasval  13376  isposix  14053  ipoval  14219  spwpr4  14302  frmdval  14435  indistopon  16700  pptbas  16707  indistpsALT  16712  tmslem  17990  sqff1o  20382  dchrval  20435  ex-uni  20756  ex-eprel  20763  subfacp1lem3  23085  subfacp1lem5  23087  umgra1  23250  vdgr1b  23267  vdgr1a  23269  eupap1  23272  eupath2lem3  23275  eupath2  23276  vdegp1ai  23280  vdegp1bi  23281  altopex  23869  altopthsn  23870  altxpsspw  23886  cbcpcp  24529  nfwpr4c  24652  cntrset  24969  pgapspf  25419  pgapspf2  25420  kelac2lem  26529  kelac2  26530  psgnghm  26804  mendval  26858  tgrpset  30101  hlhilset  31294
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-v 2765  df-dif 3130  df-un 3132  df-nul 3431  df-sn 3620  df-pr 3621
  Copyright terms: Public domain W3C validator