Theorem prex 5355

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 4703), 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 4670	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2823	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5353	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3505	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4669	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2823	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	syl5ib 243	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3521	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4701	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5354	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2847	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4702	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5354	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2847	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2106  Vcvv 3432  {csn 4561  {cpr 4563

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-sn 4562  df-pr 4564

This theorem is referenced by:  prelpw  5362  opex  5379  elopg  5381  opi2  5384  op1stb  5386  opth  5391  opeqsng  5417  opeqpr  5419  opthwiener  5428  uniop  5429  opthhausdorff  5431  opthhausdorff0  5432  fr2nr  5567  xpsspw  5719  relop  5759  f1prex  7156  unex  7596  tpex  7597  2oex  8308  pw2f1olem  8863  dif1en  8945  1sdom  9025  opthreg  9376  djuexALT  9680  pr2ne  9761  dfac2b  9886  intwun  10491  wunex2  10494  wuncval2  10503  intgru  10570  xrex  12727  seqexw  13737  pr2pwpr  14193  wwlktovfo  14673  prmreclem2  16618  prdsval  17166  xpsfval  17277  xpssca  17287  xpsvsca  17288  isposix  18043  isposixOLD  18044  clatl  18226  ipoval  18248  mgm0b  18341  frmdval  18490  mgmnsgrpex  18570  sgrpnmndex  18571  symg2bas  19000  pmtrprfval  19095  pmtrprfvalrn  19096  psgnprfval1  19130  psgnprfval2  19131  isnzr2hash  20535  psgnghm  20785  psgnco  20788  evpmodpmf1o  20801  mdetralt  21757  m2detleiblem5  21774  m2detleiblem6  21775  m2detleiblem3  21778  m2detleiblem4  21779  m2detleib  21780  indistopon  22151  pptbas  22158  indistpsALT  22163  indistpsALTOLD  22164  tuslem  23418  tuslemOLD  23419  tmslem  23637  tmslemOLD  23638  ehl2eudis  24586  sqff1o  26331  dchrval  26382  eengv  27347  structvtxvallem  27390  structiedg0val  27392  upgrbi  27463  umgrbi  27471  upgr1e  27483  umgredg  27508  uspgr1e  27611  usgr1e  27612  uspgr1ewop  27615  uspgr2v1e2w  27618  usgr2v1e2w  27619  usgrexmplef  27626  usgrexmpledg  27629  1loopgrnb0  27869  1egrvtxdg1  27876  1egrvtxdg0  27878  umgr2v2evtx  27888  umgr2v2eiedg  27890  umgr2v2e  27892  umgr2v2enb1  27893  umgr2v2evd2  27894  vdegp1ai  27903  vdegp1bi  27904  wlk2v2elem2  28520  wlk2v2e  28521  eupth2lems  28602  frcond2  28631  frcond3  28633  nfrgr2v  28636  frgr3vlem1  28637  frgr3vlem2  28638  frgrncvvdeqlem2  28664  ex-uni  28790  ex-eprel  28797  idlsrgval  31648  indf1ofs  31994  prsiga  32099  difelsiga  32101  measssd  32183  carsgsigalem  32282  carsgclctun  32288  pmeasmono  32291  eulerpartlemn  32348  probun  32386  coinflipprob  32446  coinflipspace  32447  coinfliprv  32449  coinflippv  32450  cusgredgex  33083  subfacp1lem3  33144  subfacp1lem5  33146  ex-sategoelel12  33389  altopex  34262  altopthsn  34263  altxpsspw  34279  bj-endval  35486  poimirlem9  35786  poimirlem15  35792  tgrpset  38759  hlhilset  39948  kelac2lem  40889  kelac2  40890  mendval  41008  tr3dom  41135  fvrcllb0d  41301  fvrcllb0da  41302  fvrcllb1d  41303  corclrcl  41315  corcltrcl  41347  cotrclrcl  41350  clsk1indlem2  41652  clsk1indlem3  41653  clsk1indlem4  41654  clsk1indlem1  41655  mnuprdlem3  41892  mnurndlem1  41899  prsal  43859  sge0pr  43932  elsprel  44927  sprvalpw  44932  prprvalpw  44967  sbcpr  44973  nnsum3primes4  45240  nnsum3primesgbe  45244  strisomgrop  45292  fprmappr  45681  zlmodzxzlmod  45690  zlmodzxzel  45691  zlmodzxz0  45692  zlmodzxzscm  45693  zlmodzxzadd  45694  zlmodzxzldeplem1  45841  zlmodzxzldeplem3  45843  zlmodzxzldeplem4  45844  ldepsnlinclem1  45846  ldepsnlinclem2  45847  ldepsnlinc  45849  2arymaptfo  46000  prelrrx2  46059  rrx2xpref1o  46064  rrx2plordisom  46069  ehl2eudisval0  46071  rrx2linesl  46089  2sphere0  46096  line2  46098  line2x  46100  line2y  46101  onsetreclem1  46410