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

Theorem prex 4900
 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 4293), 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 4260 . . . . . 6 (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
21eleq1d 2684 . . . . 5 (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3 zfpair2 4898 . . . . 5 {𝑥, 𝑦} ∈ V
42, 3vtoclg 3261 . . . 4 (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5 preq1 4259 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
65eleq1d 2684 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
74, 6syl5ib 234 . . 3 (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
87vtocleg 3274 . 2 (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9 prprc1 4291 . . 3 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10 snex 4899 . . 3 {𝐵} ∈ V
119, 10syl6eqel 2707 . 2 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12 prprc2 4292 . . 3 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13 snex 4899 . . 3 {𝐴} ∈ V
1412, 13syl6eqel 2707 . 2 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
158, 11, 14pm2.61nii 178 1 {𝐴, 𝐵} ∈ V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1481   ∈ wcel 1988  Vcvv 3195  {csn 4168  {cpr 4170 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570  df-un 3572  df-nul 3908  df-sn 4169  df-pr 4171 This theorem is referenced by:  prelpw  4905  opex  4923  elopg  4925  opi2  4929  op1stb  4931  opth  4935  opeqsn  4957  opeqpr  4958  propssopi  4961  opthwiener  4966  uniop  4967  fr2nr  5082  xpsspw  5223  relop  5261  f1prex  6524  unex  6941  tpex  6942  pw2f1olem  8049  1sdom  8148  opthreg  8500  pr2ne  8813  dfac2  8938  intwun  9542  wunex2  9545  wuncval2  9554  intgru  9621  xrex  11814  pr2pwpr  13244  wwlktovfo  13682  prmreclem2  15602  prdsval  16096  isposix  16938  clatl  17097  ipoval  17135  mgm0b  17237  frmdval  17369  mgmnsgrpex  17399  sgrpnmndex  17400  symg2bas  17799  pmtrprfval  17888  pmtrprfvalrn  17889  psgnprfval1  17923  psgnprfval2  17924  isnzr2hash  19245  psgnghm  19907  psgnco  19910  evpmodpmf1o  19923  mdetralt  20395  m2detleiblem5  20412  m2detleiblem6  20413  m2detleiblem3  20416  m2detleiblem4  20417  m2detleib  20418  indistopon  20786  pptbas  20793  indistpsALT  20798  tuslem  22052  tmslem  22268  sqff1o  24889  dchrval  24940  eengv  25840  structvtxvallem  25890  structiedg0val  25892  upgrbi  25969  umgrbi  25977  upgr1e  25989  umgredg  26014  uspgr1e  26117  usgr1e  26118  uspgr1ewop  26121  uspgr2v1e2w  26124  usgr2v1e2w  26125  usgrexmplef  26132  usgrexmpledg  26135  1loopgrnb0  26379  1egrvtxdg1  26386  1egrvtxdg0  26388  umgr2v2evtx  26398  umgr2v2eiedg  26400  umgr2v2e  26402  umgr2v2enb1  26403  umgr2v2evd2  26404  vdegp1ai  26413  vdegp1bi  26414  wlk2v2elem2  26996  wlk2v2e  26997  eupth2lems  27078  frcond2  27111  frcond3  27113  nfrgr2v  27116  frgr3vlem1  27117  frgr3vlem2  27118  frgrncvvdeqlem2  27144  ex-uni  27253  ex-eprel  27260  indf1ofs  30062  prsiga  30168  difelsiga  30170  inelpisys  30191  measssd  30252  carsgsigalem  30351  carsgclctun  30357  pmeasmono  30360  eulerpartlemn  30417  probun  30455  coinflipprob  30515  coinflipspace  30516  coinfliprv  30518  coinflippv  30519  subfacp1lem3  31138  subfacp1lem5  31140  altopex  32042  altopthsn  32043  altxpsspw  32059  poimirlem9  33389  poimirlem15  33395  tgrpset  35852  hlhilset  37045  kelac2lem  37453  kelac2  37454  mendval  37572  fvrcllb0d  37804  fvrcllb0da  37805  fvrcllb1d  37806  corclrcl  37818  corcltrcl  37850  cotrclrcl  37853  clsk1indlem2  38160  clsk1indlem3  38161  clsk1indlem4  38162  clsk1indlem1  38163  prsal  40301  sge0pr  40374  nnsum3primes4  41441  nnsum3primesgbe  41445  elsprel  41490  sprvalpw  41495  mapprop  41889  zlmodzxzlmod  41897  zlmodzxzel  41898  zlmodzxz0  41899  zlmodzxzscm  41900  zlmodzxzadd  41901  zlmodzxzldeplem1  42054  zlmodzxzldeplem3  42056  zlmodzxzldeplem4  42057  ldepsnlinclem1  42059  ldepsnlinclem2  42060  ldepsnlinc  42062  onsetreclem1  42213
 Copyright terms: Public domain W3C validator