Theorem prex 5437

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 4767), 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 4734	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2826	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5433	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3554	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4733	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2826	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 244	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3553	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4765	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5436	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2849	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4766	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5436	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2849	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3480  {csn 4626  {cpr 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-pr 4629

This theorem is referenced by:  prelpw  5451  opex  5469  elopg  5471  opi2  5474  op1stb  5476  opth  5481  opeqsng  5508  opeqpr  5510  opthwiener  5519  uniop  5520  opthhausdorff  5522  opthhausdorff0  5523  fr2nr  5662  xpsspw  5819  relop  5861  f1prex  7304  unexg  7763  unexOLD  7765  tpex  7766  2oex  8517  en2prd  9088  pw2f1olem  9116  dif1en  9200  dif1enOLD  9202  1sdomOLD  9285  opthreg  9658  djuexALT  9962  pr2neOLD  10045  dfac2b  10171  intwun  10775  wunex2  10778  wuncval2  10787  intgru  10854  xrex  13029  seqexw  14058  pr2pwpr  14518  wwlktovfo  14997  prmreclem2  16955  prdsval  17500  xpsfval  17611  xpssca  17621  xpsvsca  17622  isposix  18370  isposixOLD  18371  clatl  18553  ipoval  18575  mgm0b  18670  frmdval  18864  mgmnsgrpex  18944  sgrpnmndex  18945  symg2bas  19410  pmtrprfval  19505  pmtrprfvalrn  19506  psgnprfval1  19540  psgnprfval2  19541  isnzr2hash  20519  psgnghm  21598  psgnco  21601  evpmodpmf1o  21614  mdetralt  22614  m2detleiblem5  22631  m2detleiblem6  22632  m2detleiblem3  22635  m2detleiblem4  22636  m2detleib  22637  indistopon  23008  pptbas  23015  indistpsALT  23020  indistpsALTOLD  23021  tuslem  24275  tuslemOLD  24276  tmslem  24494  tmslemOLD  24495  ehl2eudis  25456  sqff1o  27225  dchrval  27278  elno  27690  eengv  28994  structvtxvallem  29037  structiedg0val  29039  upgrbi  29110  umgrbi  29118  upgr1e  29130  umgredg  29155  uspgr1e  29261  usgr1e  29262  uspgr1ewop  29265  uspgr2v1e2w  29268  usgr2v1e2w  29269  usgrexmplef  29276  usgrexmpledg  29279  1loopgrnb0  29520  1egrvtxdg1  29527  1egrvtxdg0  29529  umgr2v2evtx  29539  umgr2v2eiedg  29541  umgr2v2e  29543  umgr2v2enb1  29544  umgr2v2evd2  29545  vdegp1ai  29554  vdegp1bi  29555  wlk2v2elem2  30175  wlk2v2e  30176  eupth2lems  30257  frcond2  30286  frcond3  30288  nfrgr2v  30291  frgr3vlem1  30292  frgr3vlem2  30293  frgrncvvdeqlem2  30319  ex-uni  30445  ex-eprel  30452  indf1ofs  32851  idlsrgval  33531  constr0  33778  prsiga  34132  difelsiga  34134  measssd  34216  carsgsigalem  34317  carsgclctun  34323  pmeasmono  34326  eulerpartlemn  34383  probun  34421  coinflipprob  34482  coinflipspace  34483  coinfliprv  34485  coinflippv  34486  cusgredgex  35127  subfacp1lem3  35187  subfacp1lem5  35189  ex-sategoelel12  35432  altopex  35961  altopthsn  35962  altxpsspw  35978  bj-endval  37316  poimirlem9  37636  poimirlem15  37642  tgrpset  40747  hlhilset  41936  aprilfools2025  42684  kelac2lem  43076  kelac2  43077  mendval  43191  tr3dom  43541  fvrcllb0d  43706  fvrcllb0da  43707  fvrcllb1d  43708  corclrcl  43720  corcltrcl  43752  cotrclrcl  43755  clsk1indlem2  44055  clsk1indlem3  44056  clsk1indlem4  44057  clsk1indlem1  44058  mnuprdlem3  44293  mnurndlem1  44300  prsal  46333  sge0pr  46409  elsprel  47462  sprvalpw  47467  prprvalpw  47502  sbcpr  47508  nnsum3primes4  47775  nnsum3primesgbe  47779  opstrgric  47895  stgrfv  47920  stgredgel  47924  usgrexmpl1lem  47980  usgrexmpl1edg  47983  usgrexmpl1tri  47984  usgrexmpl2lem  47985  usgrexmpl2edg  47988  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  usgrexmpl2trifr  47996  gpgov  48001  gpgvtx  48002  gpgiedg  48003  gpgedgel  48007  fprmappr  48261  zlmodzxzlmod  48270  zlmodzxzel  48271  zlmodzxz0  48272  zlmodzxzscm  48273  zlmodzxzadd  48274  zlmodzxzldeplem1  48417  zlmodzxzldeplem3  48419  zlmodzxzldeplem4  48420  ldepsnlinclem1  48422  ldepsnlinclem2  48423  ldepsnlinc  48425  2arymaptfo  48575  prelrrx2  48634  rrx2xpref1o  48639  rrx2plordisom  48644  ehl2eudisval0  48646  rrx2linesl  48664  2sphere0  48671  line2  48673  line2x  48675  line2y  48676  termc2  49148  onsetreclem1  49224