Theorem prex 5186

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 4574), 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.

Step	Hyp	Ref	Expression
1		preq2 4541	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2845	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5184	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3481	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4540	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2845	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	syl5ib 236	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3495	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4572	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5185	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	syl6eqel 2869	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4573	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5185	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	syl6eqel 2869	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 179	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1508   ∈ wcel 2051  Vcvv 3410  {csn 4436  {cpr 4438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pr 5183

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-v 3412  df-dif 3827  df-un 3829  df-nul 4174  df-sn 4437  df-pr 4439

This theorem is referenced by:  prelpw  5192  opex  5210  elopg  5212  opi2  5215  op1stb  5217  opth  5222  opeqsng  5246  opeqpr  5248  opthwiener  5257  uniop  5258  opthhausdorff  5260  opthhausdorff0  5261  fr2nr  5382  xpsspw  5529  relop  5568  f1prex  6864  unex  7285  tpex  7286  pw2f1olem  8416  1sdom  8515  opthreg  8874  djuexALT  9144  pr2ne  9224  dfac2b  9349  intwun  9954  wunex2  9957  wuncval2  9966  intgru  10033  xrex  12200  seqexw  13199  pr2pwpr  13647  wwlktovfo  14182  prmreclem2  16108  prdsval  16583  xpsfval  16708  isposix  17438  clatl  17597  ipoval  17635  mgm0b  17737  frmdval  17870  mgmnsgrpex  17900  sgrpnmndex  17901  symg2bas  18300  pmtrprfval  18389  pmtrprfvalrn  18390  psgnprfval1  18425  psgnprfval2  18426  isnzr2hash  19771  psgnghm  20442  psgnco  20445  evpmodpmf1o  20458  mdetralt  20937  m2detleiblem5  20954  m2detleiblem6  20955  m2detleiblem3  20958  m2detleiblem4  20959  m2detleib  20960  indistopon  21329  pptbas  21336  indistpsALT  21341  tuslem  22595  tmslem  22811  ehl2eudis  23744  sqff1o  25477  dchrval  25528  eengv  26484  structvtxvallem  26524  structiedg0val  26526  upgrbi  26597  umgrbi  26605  upgr1e  26617  umgredg  26642  uspgr1e  26745  usgr1e  26746  uspgr1ewop  26749  uspgr2v1e2w  26752  usgr2v1e2w  26753  usgrexmplef  26760  usgrexmpledg  26763  1loopgrnb0  27003  1egrvtxdg1  27010  1egrvtxdg0  27012  umgr2v2evtx  27022  umgr2v2eiedg  27024  umgr2v2e  27026  umgr2v2enb1  27027  umgr2v2evd2  27028  vdegp1ai  27037  vdegp1bi  27038  wlk2v2elem2  27701  wlk2v2e  27702  eupth2lems  27784  frcond2  27817  frcond3  27819  nfrgr2v  27822  frgr3vlem1  27823  frgr3vlem2  27824  frgrncvvdeqlem2  27850  ex-uni  27999  ex-eprel  28006  indf1ofs  30962  prsiga  31068  difelsiga  31070  inelpisys  31091  measssd  31152  carsgsigalem  31251  carsgclctun  31257  pmeasmono  31260  eulerpartlemn  31317  probun  31356  coinflipprob  31416  coinflipspace  31417  coinfliprv  31419  coinflippv  31420  subfacp1lem3  32047  subfacp1lem5  32049  altopex  32975  altopthsn  32976  altxpsspw  32992  poimirlem9  34375  poimirlem15  34381  tgrpset  37359  hlhilset  38548  kelac2lem  39094  kelac2  39095  mendval  39213  fvrcllb0d  39435  fvrcllb0da  39436  fvrcllb1d  39437  corclrcl  39449  corcltrcl  39481  cotrclrcl  39484  clsk1indlem2  39789  clsk1indlem3  39790  clsk1indlem4  39791  clsk1indlem1  39792  mnuprdlem3  40019  mnurndlem1  40026  prsal  42064  sge0pr  42137  elsprel  43035  sprvalpw  43040  prprvalpw  43075  sbcpr  43081  nnsum3primes4  43351  nnsum3primesgbe  43355  strisomgrop  43403  mapprop  43788  zlmodzxzlmod  43796  zlmodzxzel  43797  zlmodzxz0  43798  zlmodzxzscm  43799  zlmodzxzadd  43800  zlmodzxzldeplem1  43952  zlmodzxzldeplem3  43954  zlmodzxzldeplem4  43955  ldepsnlinclem1  43957  ldepsnlinclem2  43958  ldepsnlinc  43960  prelrrx2  44098  rrx2xpref1o  44103  rrx2plordisom  44108  ehl2eudisval0  44110  rrx2linesl  44128  2sphere0  44135  line2  44137  line2x  44139  line2y  44140  onsetreclem1  44204