Theorem prex 5442

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 4771), 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 4738	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2823	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5438	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3553	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4737	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2823	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 244	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3552	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4769	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5441	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2846	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4770	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5441	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2846	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ∈ wcel 2105  Vcvv 3477  {csn 4630  {cpr 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-un 3967  df-nul 4339  df-sn 4631  df-pr 4633

This theorem is referenced by:  prelpw  5456  opex  5474  elopg  5476  opi2  5479  op1stb  5481  opth  5486  opeqsng  5512  opeqpr  5514  opthwiener  5523  uniop  5524  opthhausdorff  5526  opthhausdorff0  5527  fr2nr  5665  xpsspw  5821  relop  5863  f1prex  7303  unexg  7761  unexOLD  7763  tpex  7764  2oex  8515  en2prd  9086  pw2f1olem  9114  dif1en  9198  dif1enOLD  9200  1sdomOLD  9282  opthreg  9655  djuexALT  9959  pr2neOLD  10042  dfac2b  10168  intwun  10772  wunex2  10775  wuncval2  10784  intgru  10851  xrex  13026  seqexw  14054  pr2pwpr  14514  wwlktovfo  14993  prmreclem2  16950  prdsval  17501  xpsfval  17612  xpssca  17622  xpsvsca  17623  isposix  18382  isposixOLD  18383  clatl  18565  ipoval  18587  mgm0b  18682  frmdval  18876  mgmnsgrpex  18956  sgrpnmndex  18957  symg2bas  19424  pmtrprfval  19519  pmtrprfvalrn  19520  psgnprfval1  19554  psgnprfval2  19555  isnzr2hash  20535  psgnghm  21615  psgnco  21618  evpmodpmf1o  21631  mdetralt  22629  m2detleiblem5  22646  m2detleiblem6  22647  m2detleiblem3  22650  m2detleiblem4  22651  m2detleib  22652  indistopon  23023  pptbas  23030  indistpsALT  23035  indistpsALTOLD  23036  tuslem  24290  tuslemOLD  24291  tmslem  24509  tmslemOLD  24510  ehl2eudis  25469  sqff1o  27239  dchrval  27292  elno  27704  eengv  29008  structvtxvallem  29051  structiedg0val  29053  upgrbi  29124  umgrbi  29132  upgr1e  29144  umgredg  29169  uspgr1e  29275  usgr1e  29276  uspgr1ewop  29279  uspgr2v1e2w  29282  usgr2v1e2w  29283  usgrexmplef  29290  usgrexmpledg  29293  1loopgrnb0  29534  1egrvtxdg1  29541  1egrvtxdg0  29543  umgr2v2evtx  29553  umgr2v2eiedg  29555  umgr2v2e  29557  umgr2v2enb1  29558  umgr2v2evd2  29559  vdegp1ai  29568  vdegp1bi  29569  wlk2v2elem2  30184  wlk2v2e  30185  eupth2lems  30266  frcond2  30295  frcond3  30297  nfrgr2v  30300  frgr3vlem1  30301  frgr3vlem2  30302  frgrncvvdeqlem2  30328  ex-uni  30454  ex-eprel  30461  idlsrgval  33510  constr0  33741  indf1ofs  34006  prsiga  34111  difelsiga  34113  measssd  34195  carsgsigalem  34296  carsgclctun  34302  pmeasmono  34305  eulerpartlemn  34362  probun  34400  coinflipprob  34460  coinflipspace  34461  coinfliprv  34463  coinflippv  34464  cusgredgex  35105  subfacp1lem3  35166  subfacp1lem5  35168  ex-sategoelel12  35411  altopex  35941  altopthsn  35942  altxpsspw  35958  bj-endval  37297  poimirlem9  37615  poimirlem15  37621  tgrpset  40727  hlhilset  41916  aprilfools2025  42660  kelac2lem  43052  kelac2  43053  mendval  43167  tr3dom  43517  fvrcllb0d  43682  fvrcllb0da  43683  fvrcllb1d  43684  corclrcl  43696  corcltrcl  43728  cotrclrcl  43731  clsk1indlem2  44031  clsk1indlem3  44032  clsk1indlem4  44033  clsk1indlem1  44034  mnuprdlem3  44269  mnurndlem1  44276  prsal  46273  sge0pr  46349  elsprel  47399  sprvalpw  47404  prprvalpw  47439  sbcpr  47445  nnsum3primes4  47712  nnsum3primesgbe  47716  opstrgric  47832  stgrfv  47855  stgredgel  47859  usgrexmpl1lem  47915  usgrexmpl1edg  47918  usgrexmpl1tri  47919  usgrexmpl2lem  47920  usgrexmpl2edg  47923  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  usgrexmpl2trifr  47931  gpgov  47936  gpgvtx  47937  gpgiedg  47938  gpgedgel  47942  fprmappr  48189  zlmodzxzlmod  48198  zlmodzxzel  48199  zlmodzxz0  48200  zlmodzxzscm  48201  zlmodzxzadd  48202  zlmodzxzldeplem1  48345  zlmodzxzldeplem3  48347  zlmodzxzldeplem4  48348  ldepsnlinclem1  48350  ldepsnlinclem2  48351  ldepsnlinc  48353  2arymaptfo  48503  prelrrx2  48562  rrx2xpref1o  48567  rrx2plordisom  48572  ehl2eudisval0  48574  rrx2linesl  48592  2sphere0  48599  line2  48601  line2x  48603  line2y  48604  onsetreclem1  48935