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 3738), 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
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 preq2 3707 . . . . . 6  |-  ( y  =  B  ->  { x ,  y }  =  { x ,  B } )
21eleq1d 2349 . . . . 5  |-  ( y  =  B  ->  ( { x ,  y }  e.  _V  <->  { x ,  B }  e.  _V ) )
3 zfpair2 4215 . . . . 5  |-  { x ,  y }  e.  _V
42, 3vtoclg 2843 . . . 4  |-  ( B  e.  _V  ->  { x ,  B }  e.  _V )
5 preq1 3706 . . . . 5  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
65eleq1d 2349 . . . 4  |-  ( x  =  A  ->  ( { x ,  B }  e.  _V  <->  { A ,  B }  e.  _V ) )
74, 6syl5ib 210 . . 3  |-  ( x  =  A  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
87vtocleg 2854 . 2  |-  ( A  e.  _V  ->  ( B  e.  _V  ->  { A ,  B }  e.  _V ) )
9 prprc1 3736 . . 3  |-  ( -.  A  e.  _V  ->  { A ,  B }  =  { B } )
10 snex 4216 . . 3  |-  { B }  e.  _V
119, 10syl6eqel 2371 . 2  |-  ( -.  A  e.  _V  ->  { A ,  B }  e.  _V )
12 prprc2 3737 . . 3  |-  ( -.  B  e.  _V  ->  { A ,  B }  =  { A } )
13 snex 4216 . . 3  |-  { A }  e.  _V
1412, 13syl6eqel 2371 . 2  |-  ( -.  B  e.  _V  ->  { A ,  B }  e.  _V )
158, 11, 14pm2.61nii 158 1  |-  { A ,  B }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    e. wcel 1684   _Vcvv 2788   {csn 3640   {cpr 3641
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  6966  1sdom  7065  opthreg  7319  pr2ne  7635  dfac2  7757  intwun  8357  wunex2  8360  wuncval2  8369  intgru  8436  xrex  10351  prmreclem2  12964  prdsval  13355  imasval  13414  isposix  14091  ipoval  14257  spwpr4  14340  frmdval  14473  indistopon  16738  pptbas  16745  indistpsALT  16750  tmslem  18028  sqff1o  20420  dchrval  20473  ex-uni  20813  ex-eprel  20820  prelpwi  23185  prsiga  23492  difelsiga  23494  unelsiga  23495  measssd  23543  indf1ofs  23609  probun  23622  coinflipprob  23680  coinflipspace  23681  coinfliprv  23683  subfacp1lem3  23713  subfacp1lem5  23715  umgra1  23878  vdgr1b  23895  vdgr1a  23897  eupap1  23900  eupath2lem3  23903  eupath2  23904  vdegp1ai  23908  vdegp1bi  23909  altopex  24494  altopthsn  24495  altxpsspw  24511  cbcpcp  25162  nfwpr4c  25285  cntrset  25602  pgapspf  26052  pgapspf2  26053  kelac2lem  27162  kelac2  27163  psgnghm  27437  mendval  27491  prelpw  28074  uslgra1  28118  usgra1  28119  usgraedgrnv  28123  usgraexmpl  28133  frgra2v  28177  frgra3vlem1  28178  frgra3vlem2  28179  tgrpset  30934  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-un 3157  df-nul 3456  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator