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

Theorem prex 4111
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 3642), 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 3611 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2319 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4109 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 2781 . . . 4  |-  ( B  e.  _V  ->  { x ,  B }  e.  _V )
5 preq1 3610 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2319 . . . 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 2792 . 2  |-  ( A  e.  _V  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
9 prprc1 3640 . . 3  |-  ( -.  A  e.  _V  ->  { A ,  B }  =  { B } )
10 snex 4110 . . 3  |-  { B }  e.  _V
119, 10syl6eqel 2341 . 2  |-  ( -.  A  e.  _V  ->  { A ,  B }  e.  _V )
12 prprc2 3641 . . 3  |-  ( -.  B  e.  _V  ->  { A ,  B }  =  { A } )
13 snex 4110 . . 3  |-  { A }  e.  _V
1412, 13syl6eqel 2341 . 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 2727   {csn 3544   {cpr 3545
This theorem is referenced by:  opex  4130  opi2  4134  opth  4138  opeqsn  4155  opeqpr  4156  opthwiener  4161  uniop  4162  fr2nr  4264  unex  4409  tpex  4410  op1stb  4460  xpsspwOLD  4705  relop  4741  pw2f1olem  6851  1sdom  6950  opthreg  7203  pr2ne  7519  dfac2  7641  intwun  8237  wunex2  8240  wuncval2  8249  intgru  8316  xrex  10230  prmreclem2  12838  prdsval  13229  imasval  13288  isposix  13935  ipoval  14101  spwpr4  14175  frmdval  14308  indistopon  16570  pptbas  16577  indistpsALT  16582  tmslem  17860  sqff1o  20252  dchrval  20305  ex-uni  20626  ex-eprel  20633  subfacp1lem3  22884  subfacp1lem5  22886  umgra1  23049  vdgr1b  23066  vdgr1a  23068  eupap1  23071  eupath2lem3  23074  eupath2  23075  vdegp1ai  23079  vdegp1bi  23080  altopex  23668  altopthsn  23669  altxpsspw  23685  cbcpcp  24328  nfwpr4c  24451  cntrset  24768  pgapspf  25218  pgapspf2  25219  kelac2lem  26328  kelac2  26329  psgnghm  26603  mendval  26657  tgrpset  29838  hlhilset  31031
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2729  df-dif 3081  df-un 3083  df-nul 3363  df-sn 3550  df-pr 3551
  Copyright terms: Public domain W3C validator