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

Theorem prex 4826
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 4239), 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 4207 . . . . . 6 (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
21eleq1d 2666 . . . . 5 (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3 zfpair2 4824 . . . . 5 {𝑥, 𝑦} ∈ V
42, 3vtoclg 3233 . . . 4 (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5 preq1 4206 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
65eleq1d 2666 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
74, 6syl5ib 232 . . 3 (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
87vtocleg 3246 . 2 (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9 prprc1 4237 . . 3 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10 snex 4825 . . 3 {𝐵} ∈ V
119, 10syl6eqel 2690 . 2 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12 prprc2 4238 . . 3 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13 snex 4825 . . 3 {𝐴} ∈ V
1412, 13syl6eqel 2690 . 2 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
158, 11, 14pm2.61nii 176 1 {𝐴, 𝐵} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wcel 1975  Vcvv 3167  {csn 4119  {cpr 4121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-sep 4698  ax-nul 4707  ax-pr 4823
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-v 3169  df-dif 3537  df-un 3539  df-nul 3869  df-sn 4120  df-pr 4122
This theorem is referenced by:  prelpwi  4831  opex  4848  elopg  4850  opi2  4854  op1stb  4856  opth  4860  opeqsn  4881  opeqpr  4882  opthwiener  4887  uniop  4888  fr2nr  5001  xpsspw  5140  relop  5177  f1prex  6412  unex  6826  tpex  6827  pw2f1olem  7921  1sdom  8020  opthreg  8370  pr2ne  8683  dfac2  8808  intwun  9408  wunex2  9411  wuncval2  9420  intgru  9487  xrex  11656  pr2pwpr  13061  wwlktovfo  13490  prmreclem2  15400  prdsval  15879  isposix  16721  clatl  16880  ipoval  16918  mgm0b  17020  frmdval  17152  mgmnsgrpex  17182  sgrpnmndex  17183  symg2bas  17582  pmtrprfval  17671  pmtrprfvalrn  17672  psgnprfval1  17706  psgnprfval2  17707  isnzr2hash  19026  psgnghm  19685  psgnco  19688  evpmodpmf1o  19701  mdetralt  20170  m2detleiblem5  20187  m2detleiblem6  20188  m2detleiblem3  20191  m2detleiblem4  20192  m2detleib  20193  indistopon  20552  pptbas  20559  indistpsALT  20564  tuslem  21818  tmslem  22033  sqff1o  24620  dchrval  24671  eengv  25572  umgra1  25616  uslgra1  25662  usgra1  25663  usgraedgrnv  25667  usgrarnedg  25674  usgraedg4  25677  usgraexmplef  25690  usgraexmpledg  25693  cusgrarn  25749  wlkntrllem2  25851  wlkntrl  25853  constr1trl  25879  1pthon  25882  1pthon2v  25884  constr2trl  25890  constr2spth  25891  constr2pth  25892  2pthon  25893  2pthon3v  25895  usgra2adedgwlkon  25904  usg2wlk  25906  usg2wlkon  25907  constr3lem1  25934  constr3cyclpe  25952  3v3e3cycl2  25953  vdgr1b  26192  vdgr1a  26194  eupap1  26264  eupath2lem3  26267  eupath2  26268  vdegp1ai  26272  vdegp1bi  26273  frgraun  26284  frgra2v  26287  frgra3vlem1  26288  frgra3vlem2  26289  frgrancvvdeqlem3  26320  ex-uni  26436  ex-eprel  26443  indf1ofs  29216  prsiga  29322  difelsiga  29324  inelpisys  29345  measssd  29406  carsgsigalem  29505  carsgclctun  29511  pmeasmono  29514  eulerpartlemn  29571  probun  29609  coinflipprob  29669  coinflipspace  29670  coinfliprv  29672  coinflippv  29673  subfacp1lem3  30219  subfacp1lem5  30221  altopex  31038  altopthsn  31039  altxpsspw  31055  poimirlem9  32386  poimirlem15  32392  tgrpset  34849  hlhilset  36042  kelac2lem  36450  kelac2  36451  mendval  36570  fvrcllb0d  36802  fvrcllb0da  36803  fvrcllb1d  36804  corclrcl  36816  corcltrcl  36848  cotrclrcl  36851  clsk1indlem2  37158  clsk1indlem3  37159  clsk1indlem4  37160  clsk1indlem1  37161  prsal  39013  sge0pr  39086  nnsum3primes4  40004  nnsum3primesgbe  40008  prelpw  40115  propssopi  40122  structvtxvallem  40250  structiedg0val  40252  upgrbi  40316  umgrbi  40323  upgr1e  40335  edgastruct  40353  umgredg  40368  uspgr1e  40467  usgr1e  40468  uspgr1ewop  40471  uspgr2v1e2w  40474  usgr2v1e2w  40475  usgrexmpledg  40483  1loopgrnb0  40714  1egrvtxdg1  40722  1egrvtxdg0  40724  umgr2v2evtx  40734  umgr2v2eiedg  40736  umgr2v2e  40738  umgr2v2enb1  40739  umgr2v2evd2  40740  vdegp1ai-av  40749  vdegp1bi-av  40750  1wlk2v2elem2  41320  1wlk2v2e  41321  eupth2lems  41403  frcond2  41436  nfrgr2v  41439  frgr3vlem1  41440  frgr3vlem2  41441  frgrncvvdeqlem3  41468  mapprop  41914  zlmodzxzlmod  41922  zlmodzxzel  41923  zlmodzxz0  41924  zlmodzxzscm  41925  zlmodzxzadd  41926  zlmodzxzldeplem1  42080  zlmodzxzldeplem3  42082  zlmodzxzldeplem4  42083  ldepsnlinclem1  42085  ldepsnlinclem2  42086  ldepsnlinc  42088
  Copyright terms: Public domain W3C validator