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

Theorem prex 5065
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 4457), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
prex {𝐴, 𝐵} ∈ V

Proof of Theorem prex
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 preq2 4424 . . . . . 6 (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
21eleq1d 2829 . . . . 5 (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3 zfpair2 5063 . . . . 5 {𝑥, 𝑦} ∈ V
42, 3vtoclg 3418 . . . 4 (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5 preq1 4423 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
65eleq1d 2829 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
74, 6syl5ib 235 . . 3 (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
87vtocleg 3431 . 2 (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9 prprc1 4455 . . 3 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10 snex 5064 . . 3 {𝐵} ∈ V
119, 10syl6eqel 2852 . 2 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12 prprc2 4456 . . 3 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13 snex 5064 . . 3 {𝐴} ∈ V
1412, 13syl6eqel 2852 . 2 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
158, 11, 14pm2.61nii 178 1 {𝐴, 𝐵} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1652  wcel 2155  Vcvv 3350  {csn 4334  {cpr 4336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-dif 3735  df-un 3737  df-nul 4080  df-sn 4335  df-pr 4337
This theorem is referenced by:  prelpw  5070  opex  5088  elopg  5090  opi2  5093  op1stb  5095  opth  5100  opeqsng  5122  opeqsnOLD  5124  opeqpr  5125  opthwiener  5135  uniop  5136  opthhausdorff  5138  opthhausdorff0  5139  fr2nr  5255  xpsspw  5401  relop  5441  f1prex  6731  unex  7154  tpex  7155  pw2f1olem  8271  1sdom  8370  opthreg  8728  opthregOLD  8730  djuexALT  8999  pr2ne  9079  dfac2b  9204  dfac2OLD  9206  intwun  9810  wunex2  9813  wuncval2  9822  intgru  9889  xrex  12025  pr2pwpr  13462  wwlktovfo  13990  prmreclem2  15902  prdsval  16383  isposix  17225  clatl  17384  ipoval  17422  mgm0b  17524  frmdval  17657  mgmnsgrpex  17687  sgrpnmndex  17688  symg2bas  18083  pmtrprfval  18172  pmtrprfvalrn  18173  psgnprfval1  18208  psgnprfval2  18209  isnzr2hash  19538  psgnghm  20198  psgnco  20201  evpmodpmf1o  20215  mdetralt  20691  m2detleiblem5  20708  m2detleiblem6  20709  m2detleiblem3  20712  m2detleiblem4  20713  m2detleib  20714  indistopon  21085  pptbas  21092  indistpsALT  21097  tuslem  22350  tmslem  22566  sqff1o  25199  dchrval  25250  eengv  26150  structvtxvallem  26189  structiedg0val  26191  upgrbi  26265  umgrbi  26273  upgr1e  26285  umgredg  26311  uspgr1e  26415  usgr1e  26416  uspgr1ewop  26419  uspgr2v1e2w  26422  usgr2v1e2w  26423  usgrexmplef  26430  usgrexmpledg  26433  1loopgrnb0  26689  1egrvtxdg1  26696  1egrvtxdg0  26698  umgr2v2evtx  26708  umgr2v2eiedg  26710  umgr2v2e  26712  umgr2v2enb1  26713  umgr2v2evd2  26714  vdegp1ai  26723  vdegp1bi  26724  wlk2v2elem2  27392  wlk2v2e  27393  eupth2lems  27474  frcond2  27505  frcond3  27507  nfrgr2v  27510  frgr3vlem1  27511  frgr3vlem2  27512  frgrncvvdeqlem2  27538  ex-uni  27677  ex-eprel  27684  indf1ofs  30470  prsiga  30576  difelsiga  30578  inelpisys  30599  measssd  30660  carsgsigalem  30759  carsgclctun  30765  pmeasmono  30768  eulerpartlemn  30825  probun  30864  coinflipprob  30924  coinflipspace  30925  coinfliprv  30927  coinflippv  30928  subfacp1lem3  31544  subfacp1lem5  31546  altopex  32443  altopthsn  32444  altxpsspw  32460  poimirlem9  33774  poimirlem15  33780  tgrpset  36633  hlhilset  37822  kelac2lem  38243  kelac2  38244  mendval  38362  fvrcllb0d  38592  fvrcllb0da  38593  fvrcllb1d  38594  corclrcl  38606  corcltrcl  38638  cotrclrcl  38641  clsk1indlem2  38946  clsk1indlem3  38947  clsk1indlem4  38948  clsk1indlem1  38949  prsal  41107  sge0pr  41180  nnsum3primes4  42284  nnsum3primesgbe  42288  elsprel  42326  sprvalpw  42331  mapprop  42725  zlmodzxzlmod  42733  zlmodzxzel  42734  zlmodzxz0  42735  zlmodzxzscm  42736  zlmodzxzadd  42737  zlmodzxzldeplem1  42890  zlmodzxzldeplem3  42892  zlmodzxzldeplem4  42893  ldepsnlinclem1  42895  ldepsnlinclem2  42896  ldepsnlinc  42898  onsetreclem1  43052
  Copyright terms: Public domain W3C validator