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

Theorem prex 5324
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 4697), 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 4664 . . . . . 6 (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
21eleq1d 2897 . . . . 5 (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3 zfpair2 5322 . . . . 5 {𝑥, 𝑦} ∈ V
42, 3vtoclg 3568 . . . 4 (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5 preq1 4663 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
65eleq1d 2897 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
74, 6syl5ib 245 . . 3 (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
87vtocleg 3581 . 2 (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9 prprc1 4695 . . 3 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10 snex 5323 . . 3 {𝐵} ∈ V
119, 10syl6eqel 2921 . 2 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12 prprc2 4696 . . 3 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13 snex 5323 . . 3 {𝐴} ∈ V
1412, 13syl6eqel 2921 . 2 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
158, 11, 14pm2.61nii 185 1 {𝐴, 𝐵} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wcel 2105  Vcvv 3495  {csn 4559  {cpr 4561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-dif 3938  df-un 3940  df-nul 4291  df-sn 4560  df-pr 4562
This theorem is referenced by:  prelpw  5330  opex  5348  elopg  5350  opi2  5353  op1stb  5355  opth  5360  opeqsng  5385  opeqpr  5387  opthwiener  5396  uniop  5397  opthhausdorff  5399  opthhausdorff0  5400  fr2nr  5527  xpsspw  5676  relop  5715  f1prex  7031  unex  7457  tpex  7458  pw2f1olem  8610  1sdom  8710  opthreg  9070  djuexALT  9340  pr2ne  9420  dfac2b  9545  intwun  10146  wunex2  10149  wuncval2  10158  intgru  10225  xrex  12376  seqexw  13375  pr2pwpr  13827  wwlktovfo  14312  prmreclem2  16243  prdsval  16718  xpsfval  16829  xpssca  16839  xpsvsca  16840  isposix  17557  clatl  17716  ipoval  17754  mgm0b  17857  frmdval  18006  mgmnsgrpex  18036  sgrpnmndex  18037  symg2bas  18457  pmtrprfval  18546  pmtrprfvalrn  18547  psgnprfval1  18581  psgnprfval2  18582  isnzr2hash  19967  psgnghm  20654  psgnco  20657  evpmodpmf1o  20670  mdetralt  21147  m2detleiblem5  21164  m2detleiblem6  21165  m2detleiblem3  21168  m2detleiblem4  21169  m2detleib  21170  indistopon  21539  pptbas  21546  indistpsALT  21551  tuslem  22805  tmslem  23021  ehl2eudis  23954  sqff1o  25687  dchrval  25738  eengv  26693  structvtxvallem  26733  structiedg0val  26735  upgrbi  26806  umgrbi  26814  upgr1e  26826  umgredg  26851  uspgr1e  26954  usgr1e  26955  uspgr1ewop  26958  uspgr2v1e2w  26961  usgr2v1e2w  26962  usgrexmplef  26969  usgrexmpledg  26972  1loopgrnb0  27212  1egrvtxdg1  27219  1egrvtxdg0  27221  umgr2v2evtx  27231  umgr2v2eiedg  27233  umgr2v2e  27235  umgr2v2enb1  27236  umgr2v2evd2  27237  vdegp1ai  27246  vdegp1bi  27247  wlk2v2elem2  27863  wlk2v2e  27864  eupth2lems  27945  frcond2  27974  frcond3  27976  nfrgr2v  27979  frgr3vlem1  27980  frgr3vlem2  27981  frgrncvvdeqlem2  28007  ex-uni  28133  ex-eprel  28140  indf1ofs  31185  prsiga  31290  difelsiga  31292  inelpisys  31313  measssd  31374  carsgsigalem  31473  carsgclctun  31479  pmeasmono  31482  eulerpartlemn  31539  probun  31577  coinflipprob  31637  coinflipspace  31638  coinfliprv  31640  coinflippv  31641  cusgredgex  32266  subfacp1lem3  32327  subfacp1lem5  32329  ex-sategoelel12  32572  altopex  33319  altopthsn  33320  altxpsspw  33336  poimirlem9  34783  poimirlem15  34789  tgrpset  37763  hlhilset  38952  kelac2lem  39544  kelac2  39545  mendval  39663  tr3dom  39774  fvrcllb0d  39918  fvrcllb0da  39919  fvrcllb1d  39920  corclrcl  39932  corcltrcl  39964  cotrclrcl  39967  clsk1indlem2  40272  clsk1indlem3  40273  clsk1indlem4  40274  clsk1indlem1  40275  mnuprdlem3  40490  mnurndlem1  40497  prsal  42484  sge0pr  42557  elsprel  43484  sprvalpw  43489  prprvalpw  43524  sbcpr  43530  nnsum3primes4  43800  nnsum3primesgbe  43804  strisomgrop  43852  mapprop  44292  zlmodzxzlmod  44300  zlmodzxzel  44301  zlmodzxz0  44302  zlmodzxzscm  44303  zlmodzxzadd  44304  zlmodzxzldeplem1  44453  zlmodzxzldeplem3  44455  zlmodzxzldeplem4  44456  ldepsnlinclem1  44458  ldepsnlinclem2  44459  ldepsnlinc  44461  prelrrx2  44598  rrx2xpref1o  44603  rrx2plordisom  44608  ehl2eudisval0  44610  rrx2linesl  44628  2sphere0  44635  line2  44637  line2x  44639  line2y  44640  onsetreclem1  44705
  Copyright terms: Public domain W3C validator