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

Theorem prex 4694
 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 4142), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
prex

Proof of Theorem prex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 preq2 4110 . . . . . 6
21eleq1d 2526 . . . . 5
3 zfpair2 4692 . . . . 5
42, 3vtoclg 3167 . . . 4
5 preq1 4109 . . . . 5
65eleq1d 2526 . . . 4
74, 6syl5ib 219 . . 3
87vtocleg 3180 . 2
9 prprc1 4140 . . 3
10 snex 4693 . . 3
119, 10syl6eqel 2553 . 2
12 prprc2 4141 . . 3
13 snex 4693 . . 3
1412, 13syl6eqel 2553 . 2
158, 11, 14pm2.61nii 166 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  e.wcel 1818   cvv 3109  {csn 4029  {cpr 4031 This theorem is referenced by:  prelpwi  4699  opex  4716  opi2  4720  op1stb  4722  opth  4726  opeqsn  4748  opeqpr  4749  opthwiener  4754  uniop  4755  fr2nr  4862  xpsspwOLD  5122  relop  5158  unex  6598  tpex  6599  pw2f1olem  7641  1sdom  7742  opthreg  8056  pr2ne  8404  dfac2  8532  intwun  9134  wunex2  9137  wuncval2  9146  intgru  9213  xrex  11246  pr2pwpr  12520  wwlktovfo  12896  prmreclem2  14435  prdsval  14852  isposix  15587  clatl  15746  ipoval  15784  frmdval  16019  mgmnsgrpex  16049  sgrpnmndex  16050  symg2bas  16423  pmtrprfval  16512  pmtrprfvalrn  16513  psgnprfval1  16547  psgnprfval2  16548  isnzr2hash  17912  psgnghm  18616  psgnco  18619  evpmodpmf1o  18632  mdetralt  19110  m2detleiblem5  19127  m2detleiblem6  19128  m2detleiblem3  19131  m2detleiblem4  19132  m2detleib  19133  indistopon  19502  pptbas  19509  indistpsALT  19514  tuslem  20770  tmslem  20985  sqff1o  23456  dchrval  23509  eengv  24282  umgra1  24326  uslgra1  24372  usgra1  24373  usgraedgrnv  24377  usgrarnedg  24384  usgraedg4  24387  usgraexmpl  24401  usgraexmpledg  24403  cusgrarn  24459  wlkntrllem2  24562  wlkntrl  24564  constr1trl  24590  1pthon  24593  1pthon2v  24595  constr2trl  24601  constr2spth  24602  constr2pth  24603  2pthon  24604  2pthon3v  24606  usgra2adedgwlkon  24615  usg2wlk  24617  usg2wlkon  24618  constr3lem1  24645  constr3cyclpe  24663  3v3e3cycl2  24664  vdgr1b  24904  vdgr1a  24906  eupap1  24976  eupath2lem3  24979  eupath2  24980  vdegp1ai  24984  vdegp1bi  24985  frgraun  24996  frgra2v  24999  frgra3vlem1  25000  frgra3vlem2  25001  frgrancvvdeqlem3  25032  ex-uni  25147  ex-eprel  25154  indf1ofs  28039  prsiga  28131  difelsiga  28133  measssd  28186  eulerpartlemn  28320  probun  28358  coinflipprob  28418  coinflipspace  28419  coinfliprv  28421  coinflippv  28422  subfacp1lem3  28626  subfacp1lem5  28628  altopex  29610  altopthsn  29611  altxpsspw  29627  kelac2lem  31010  kelac2  31011  mendval  31132  prelpw  32299  mapprop  32935  zlmodzxzlmod  32943  zlmodzxzel  32944  zlmodzxz0  32945  zlmodzxzscm  32946  zlmodzxzadd  32947  zlmodzxzldeplem1  33101  zlmodzxzldeplem3  33103  zlmodzxzldeplem4  33104  ldepsnlinclem1  33106  ldepsnlinclem2  33107  ldepsnlinc  33109  bj-elopg  34602  tgrpset  36471  hlhilset  37664 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-un 3480  df-nul 3785  df-sn 4030  df-pr 4032
 Copyright terms: Public domain W3C validator