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

Theorem prex 4217
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 3740), 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
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem prex
StepHypRef Expression
1 preq2 3709 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2351 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4215 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 2845 . . . 4  |-  ( B  e.  _V  ->  { x ,  B }  e.  _V )
5 preq1 3708 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2351 . . . 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 2856 . 2  |-  ( A  e.  _V  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
9 prprc1 3738 . . 3  |-  ( -.  A  e.  _V  ->  { A ,  B }  =  { B } )
10 snex 4216 . . 3  |-  { B }  e.  _V
119, 10syl6eqel 2373 . 2  |-  ( -.  A  e.  _V  ->  { A ,  B }  e.  _V )
12 prprc2 3739 . . 3  |-  ( -.  B  e.  _V  ->  { A ,  B }  =  { A } )
13 snex 4216 . . 3  |-  { A }  e.  _V
1412, 13syl6eqel 2373 . 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 1624    e. wcel 1685   _Vcvv 2790   {csn 3642   {cpr 3643
This theorem is referenced by:  opex  4237  opi2  4241  opth  4245  opeqsn  4262  opeqpr  4263  opthwiener  4268  uniop  4269  fr2nr  4371  unex  4518  tpex  4519  op1stb  4569  xpsspwOLD  4798  relop  4834  pw2f1olem  6962  1sdom  7061  opthreg  7315  pr2ne  7631  dfac2  7753  intwun  8353  wunex2  8356  wuncval2  8365  intgru  8432  xrex  10347  prmreclem2  12959  prdsval  13350  imasval  13409  isposix  14086  ipoval  14252  spwpr4  14335  frmdval  14468  indistopon  16733  pptbas  16740  indistpsALT  16745  tmslem  18023  sqff1o  20415  dchrval  20468  ex-uni  20789  ex-eprel  20796  subfacp1lem3  23118  subfacp1lem5  23120  umgra1  23283  vdgr1b  23300  vdgr1a  23302  eupap1  23305  eupath2lem3  23308  eupath2  23309  vdegp1ai  23313  vdegp1bi  23314  altopex  23902  altopthsn  23903  altxpsspw  23919  cbcpcp  24562  nfwpr4c  24685  cntrset  25002  pgapspf  25452  pgapspf2  25453  kelac2lem  26562  kelac2  26563  psgnghm  26837  mendval  26891  tgrpset  30202  hlhilset  31395
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4214
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-v 2792  df-dif 3157  df-un 3159  df-nul 3458  df-sn 3648  df-pr 3649
  Copyright terms: Public domain W3C validator