Theorem prex 5433

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 4772), 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 4739	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2819	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5429	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3557	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4738	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2819	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 243	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3546	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4770	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5432	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2842	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4771	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5432	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2842	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4629  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-un 3954  df-nul 4324  df-sn 4630  df-pr 4632

This theorem is referenced by:  prelpw  5447  opex  5465  elopg  5467  opi2  5470  op1stb  5472  opth  5477  opeqsng  5504  opeqpr  5506  opthwiener  5515  uniop  5516  opthhausdorff  5518  opthhausdorff0  5519  fr2nr  5655  xpsspw  5810  relop  5851  f1prex  7282  unex  7733  tpex  7734  2oex  8477  en2prd  9048  pw2f1olem  9076  dif1en  9160  dif1enOLD  9162  1sdomOLD  9249  opthreg  9613  djuexALT  9917  pr2neOLD  10000  dfac2b  10125  intwun  10730  wunex2  10733  wuncval2  10742  intgru  10809  xrex  12971  seqexw  13982  pr2pwpr  14440  wwlktovfo  14909  prmreclem2  16850  prdsval  17401  xpsfval  17512  xpssca  17522  xpsvsca  17523  isposix  18278  isposixOLD  18279  clatl  18461  ipoval  18483  mgm0b  18576  frmdval  18732  mgmnsgrpex  18812  sgrpnmndex  18813  symg2bas  19260  pmtrprfval  19355  pmtrprfvalrn  19356  psgnprfval1  19390  psgnprfval2  19391  isnzr2hash  20298  psgnghm  21133  psgnco  21136  evpmodpmf1o  21149  mdetralt  22110  m2detleiblem5  22127  m2detleiblem6  22128  m2detleiblem3  22131  m2detleiblem4  22132  m2detleib  22133  indistopon  22504  pptbas  22511  indistpsALT  22516  indistpsALTOLD  22517  tuslem  23771  tuslemOLD  23772  tmslem  23990  tmslemOLD  23991  ehl2eudis  24939  sqff1o  26686  dchrval  26737  eengv  28237  structvtxvallem  28280  structiedg0val  28282  upgrbi  28353  umgrbi  28361  upgr1e  28373  umgredg  28398  uspgr1e  28501  usgr1e  28502  uspgr1ewop  28505  uspgr2v1e2w  28508  usgr2v1e2w  28509  usgrexmplef  28516  usgrexmpledg  28519  1loopgrnb0  28759  1egrvtxdg1  28766  1egrvtxdg0  28768  umgr2v2evtx  28778  umgr2v2eiedg  28780  umgr2v2e  28782  umgr2v2enb1  28783  umgr2v2evd2  28784  vdegp1ai  28793  vdegp1bi  28794  wlk2v2elem2  29409  wlk2v2e  29410  eupth2lems  29491  frcond2  29520  frcond3  29522  nfrgr2v  29525  frgr3vlem1  29526  frgr3vlem2  29527  frgrncvvdeqlem2  29553  ex-uni  29679  ex-eprel  29686  idlsrgval  32617  indf1ofs  33024  prsiga  33129  difelsiga  33131  measssd  33213  carsgsigalem  33314  carsgclctun  33320  pmeasmono  33323  eulerpartlemn  33380  probun  33418  coinflipprob  33478  coinflipspace  33479  coinfliprv  33481  coinflippv  33482  cusgredgex  34112  subfacp1lem3  34173  subfacp1lem5  34175  ex-sategoelel12  34418  altopex  34932  altopthsn  34933  altxpsspw  34949  bj-endval  36196  poimirlem9  36497  poimirlem15  36503  tgrpset  39616  hlhilset  40805  aprilfools2025  41416  kelac2lem  41806  kelac2  41807  mendval  41925  tr3dom  42279  fvrcllb0d  42444  fvrcllb0da  42445  fvrcllb1d  42446  corclrcl  42458  corcltrcl  42490  cotrclrcl  42493  clsk1indlem2  42793  clsk1indlem3  42794  clsk1indlem4  42795  clsk1indlem1  42796  mnuprdlem3  43033  mnurndlem1  43040  prsal  45034  sge0pr  45110  elsprel  46143  sprvalpw  46148  prprvalpw  46183  sbcpr  46189  nnsum3primes4  46456  nnsum3primesgbe  46460  strisomgrop  46508  fprmappr  47021  zlmodzxzlmod  47030  zlmodzxzel  47031  zlmodzxz0  47032  zlmodzxzscm  47033  zlmodzxzadd  47034  zlmodzxzldeplem1  47181  zlmodzxzldeplem3  47183  zlmodzxzldeplem4  47184  ldepsnlinclem1  47186  ldepsnlinclem2  47187  ldepsnlinc  47189  2arymaptfo  47340  prelrrx2  47399  rrx2xpref1o  47404  rrx2plordisom  47409  ehl2eudisval0  47411  rrx2linesl  47429  2sphere0  47436  line2  47438  line2x  47440  line2y  47441  onsetreclem1  47750