Theorem prex 5375

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 4720), 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 4687	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2816	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5371	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3509	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4686	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2816	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 244	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3508	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4718	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5374	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2839	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4719	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5374	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2839	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2111  Vcvv 3436  {csn 4576  {cpr 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-un 3907  df-nul 4284  df-sn 4577  df-pr 4579

This theorem is referenced by:  prelpw  5387  opex  5404  elopg  5406  opi2  5409  op1stb  5411  opth  5416  opeqsng  5443  opeqpr  5445  opthwiener  5454  uniop  5455  opthhausdorff  5457  opthhausdorff0  5458  fr2nr  5593  xpsspw  5749  relop  5790  f1prex  7218  unexg  7676  unexOLD  7678  tpex  7679  2oex  8396  en2prd  8969  pw2f1olem  8994  dif1en  9071  opthreg  9508  djuexALT  9812  dfac2b  10019  intwun  10623  wunex2  10626  wuncval2  10635  intgru  10702  xrex  12882  seqexw  13921  pr2pwpr  14383  wwlktovfo  14862  prmreclem2  16826  prdsval  17356  xpsfval  17467  xpssca  17477  xpsvsca  17478  isposix  18227  clatl  18411  ipoval  18433  mgm0b  18562  frmdval  18756  mgmnsgrpex  18836  sgrpnmndex  18837  symg2bas  19303  pmtrprfval  19397  pmtrprfvalrn  19398  psgnprfval1  19432  psgnprfval2  19433  isnzr2hash  20432  psgnghm  21515  psgnco  21518  evpmodpmf1o  21531  mdetralt  22521  m2detleiblem5  22538  m2detleiblem6  22539  m2detleiblem3  22542  m2detleiblem4  22543  m2detleib  22544  indistopon  22914  pptbas  22921  indistpsALT  22926  tuslem  24179  tmslem  24395  ehl2eudis  25347  sqff1o  27117  dchrval  27170  elno  27582  eengv  28955  structvtxvallem  28996  structiedg0val  28998  upgrbi  29069  umgrbi  29077  upgr1e  29089  umgredg  29114  uspgr1e  29220  usgr1e  29221  uspgr1ewop  29224  uspgr2v1e2w  29227  usgr2v1e2w  29228  usgrexmplef  29235  usgrexmpledg  29238  1loopgrnb0  29479  1egrvtxdg1  29486  1egrvtxdg0  29488  umgr2v2evtx  29498  umgr2v2eiedg  29500  umgr2v2e  29502  umgr2v2enb1  29503  umgr2v2evd2  29504  vdegp1ai  29513  vdegp1bi  29514  wlk2v2elem2  30131  wlk2v2e  30132  eupth2lems  30213  frcond2  30242  frcond3  30244  nfrgr2v  30247  frgr3vlem1  30248  frgr3vlem2  30249  frgrncvvdeqlem2  30275  ex-uni  30401  ex-eprel  30408  indf1ofs  32842  idlsrgval  33463  constr0  33745  prsiga  34139  difelsiga  34141  measssd  34223  carsgsigalem  34323  carsgclctun  34329  pmeasmono  34332  eulerpartlemn  34389  probun  34427  coinflipprob  34488  coinflipspace  34489  coinfliprv  34491  coinflippv  34492  cusgredgex  35154  subfacp1lem3  35214  subfacp1lem5  35216  ex-sategoelel12  35459  altopex  35993  altopthsn  35994  altxpsspw  36010  bj-endval  37348  poimirlem9  37668  poimirlem15  37674  tgrpset  40783  hlhilset  41972  aprilfools2025  42706  kelac2lem  43096  kelac2  43097  mendval  43211  tr3dom  43560  fvrcllb0d  43725  fvrcllb0da  43726  fvrcllb1d  43727  corclrcl  43739  corcltrcl  43771  cotrclrcl  43774  clsk1indlem2  44074  clsk1indlem3  44075  clsk1indlem4  44076  clsk1indlem1  44077  mnuprdlem3  44306  mnurndlem1  44313  permaxpr  45042  prsal  46355  sge0pr  46431  elsprel  47505  sprvalpw  47510  prprvalpw  47545  sbcpr  47551  nnsum3primes4  47818  nnsum3primesgbe  47822  opstrgric  47956  stgrfv  47983  stgredgel  47987  usgrexmpl1lem  48051  usgrexmpl1edg  48054  usgrexmpl1tri  48055  usgrexmpl2lem  48056  usgrexmpl2edg  48059  usgrexmpl2nb0  48061  usgrexmpl2nb1  48062  usgrexmpl2nb2  48063  usgrexmpl2nb3  48064  usgrexmpl2nb4  48065  usgrexmpl2nb5  48066  usgrexmpl2trifr  48067  gpgov  48072  gpgvtx  48073  gpgiedg  48074  gpgiedgdmellem  48076  gpgprismgr4cycllem2  48126  gpgprismgr4cycllem3  48127  gpgprismgr4cycllem8  48132  gpgprismgr4cycllem10  48134  pgnbgreunbgr  48155  fprmappr  48375  zlmodzxzlmod  48384  zlmodzxzel  48385  zlmodzxz0  48386  zlmodzxzscm  48387  zlmodzxzadd  48388  zlmodzxzldeplem1  48531  zlmodzxzldeplem3  48533  zlmodzxzldeplem4  48534  ldepsnlinclem1  48536  ldepsnlinclem2  48537  ldepsnlinc  48539  2arymaptfo  48685  prelrrx2  48744  rrx2xpref1o  48749  rrx2plordisom  48754  ehl2eudisval0  48756  rrx2linesl  48774  2sphere0  48781  line2  48783  line2x  48785  line2y  48786  resipos  49005  fucoppcffth  49442  termc2  49549  uobeqterm  49577  incat  49632  onsetreclem1  49736