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

Theorem prex 5387
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 4726), 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 4693 . . . . . 6 (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
21eleq1d 2822 . . . . 5 (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3 zfpair2 5383 . . . . 5 {𝑥, 𝑦} ∈ V
42, 3vtoclg 3523 . . . 4 (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5 preq1 4692 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
65eleq1d 2822 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
74, 6syl5ib 243 . . 3 (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
87vtocleg 3512 . 2 (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9 prprc1 4724 . . 3 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10 snex 5386 . . 3 {𝐵} ∈ V
119, 10eqeltrdi 2846 . 2 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12 prprc2 4725 . . 3 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13 snex 5386 . . 3 {𝐴} ∈ V
1412, 13eqeltrdi 2846 . 2 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
158, 11, 14pm2.61nii 184 1 {𝐴, 𝐵} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1541  wcel 2106  Vcvv 3443  {csn 4584  {cpr 4586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-dif 3911  df-un 3913  df-nul 4281  df-sn 4585  df-pr 4587
This theorem is referenced by:  prelpw  5401  opex  5419  elopg  5421  opi2  5424  op1stb  5426  opth  5431  opeqsng  5457  opeqpr  5459  opthwiener  5468  uniop  5469  opthhausdorff  5471  opthhausdorff0  5472  fr2nr  5608  xpsspw  5761  relop  5802  f1prex  7224  unex  7670  tpex  7671  2oex  8390  en2prd  8925  pw2f1olem  8953  dif1en  9037  dif1enOLD  9039  1sdomOLD  9126  opthreg  9487  djuexALT  9791  pr2neOLD  9874  dfac2b  9999  intwun  10604  wunex2  10607  wuncval2  10616  intgru  10683  xrex  12840  seqexw  13850  pr2pwpr  14305  wwlktovfo  14780  prmreclem2  16723  prdsval  17271  xpsfval  17382  xpssca  17392  xpsvsca  17393  isposix  18148  isposixOLD  18149  clatl  18331  ipoval  18353  mgm0b  18446  frmdval  18595  mgmnsgrpex  18675  sgrpnmndex  18676  symg2bas  19106  pmtrprfval  19201  pmtrprfvalrn  19202  psgnprfval1  19236  psgnprfval2  19237  isnzr2hash  20657  psgnghm  20907  psgnco  20910  evpmodpmf1o  20923  mdetralt  21879  m2detleiblem5  21896  m2detleiblem6  21897  m2detleiblem3  21900  m2detleiblem4  21901  m2detleib  21902  indistopon  22273  pptbas  22280  indistpsALT  22285  indistpsALTOLD  22286  tuslem  23540  tuslemOLD  23541  tmslem  23759  tmslemOLD  23760  ehl2eudis  24708  sqff1o  26453  dchrval  26504  eengv  27726  structvtxvallem  27769  structiedg0val  27771  upgrbi  27842  umgrbi  27850  upgr1e  27862  umgredg  27887  uspgr1e  27990  usgr1e  27991  uspgr1ewop  27994  uspgr2v1e2w  27997  usgr2v1e2w  27998  usgrexmplef  28005  usgrexmpledg  28008  1loopgrnb0  28248  1egrvtxdg1  28255  1egrvtxdg0  28257  umgr2v2evtx  28267  umgr2v2eiedg  28269  umgr2v2e  28271  umgr2v2enb1  28272  umgr2v2evd2  28273  vdegp1ai  28282  vdegp1bi  28283  wlk2v2elem2  28898  wlk2v2e  28899  eupth2lems  28980  frcond2  29009  frcond3  29011  nfrgr2v  29014  frgr3vlem1  29015  frgr3vlem2  29016  frgrncvvdeqlem2  29042  ex-uni  29168  ex-eprel  29175  idlsrgval  32034  indf1ofs  32398  prsiga  32503  difelsiga  32505  measssd  32587  carsgsigalem  32688  carsgclctun  32694  pmeasmono  32697  eulerpartlemn  32754  probun  32792  coinflipprob  32852  coinflipspace  32853  coinfliprv  32855  coinflippv  32856  cusgredgex  33488  subfacp1lem3  33549  subfacp1lem5  33551  ex-sategoelel12  33794  altopex  34440  altopthsn  34441  altxpsspw  34457  bj-endval  35681  poimirlem9  35982  poimirlem15  35988  tgrpset  39103  hlhilset  40292  kelac2lem  41256  kelac2  41257  mendval  41375  tr3dom  41562  fvrcllb0d  41727  fvrcllb0da  41728  fvrcllb1d  41729  corclrcl  41741  corcltrcl  41773  cotrclrcl  41776  clsk1indlem2  42078  clsk1indlem3  42079  clsk1indlem4  42080  clsk1indlem1  42081  mnuprdlem3  42318  mnurndlem1  42325  prsal  44312  sge0pr  44388  elsprel  45416  sprvalpw  45421  prprvalpw  45456  sbcpr  45462  nnsum3primes4  45729  nnsum3primesgbe  45733  strisomgrop  45781  fprmappr  46170  zlmodzxzlmod  46179  zlmodzxzel  46180  zlmodzxz0  46181  zlmodzxzscm  46182  zlmodzxzadd  46183  zlmodzxzldeplem1  46330  zlmodzxzldeplem3  46332  zlmodzxzldeplem4  46333  ldepsnlinclem1  46335  ldepsnlinclem2  46336  ldepsnlinc  46338  2arymaptfo  46489  prelrrx2  46548  rrx2xpref1o  46553  rrx2plordisom  46558  ehl2eudisval0  46560  rrx2linesl  46578  2sphere0  46585  line2  46587  line2x  46589  line2y  46590  onsetreclem1  46898
  Copyright terms: Public domain W3C validator