Theorem prex 5333

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 2897	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5331	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3567	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4669	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2897	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	syl5ib 246	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3581	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4701	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5332	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2921	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4702	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5332	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2921	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 186	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2114  Vcvv 3494  {csn 4567  {cpr 4569

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-un 3941  df-nul 4292  df-sn 4568  df-pr 4570

This theorem is referenced by:  prelpw  5339  opex  5356  elopg  5358  opi2  5361  op1stb  5363  opth  5368  opeqsng  5393  opeqpr  5395  opthwiener  5404  uniop  5405  opthhausdorff  5407  opthhausdorff0  5408  fr2nr  5533  xpsspw  5682  relop  5721  f1prex  7040  unex  7469  tpex  7470  pw2f1olem  8621  1sdom  8721  opthreg  9081  djuexALT  9351  pr2ne  9431  dfac2b  9556  intwun  10157  wunex2  10160  wuncval2  10169  intgru  10236  xrex  12387  seqexw  13386  pr2pwpr  13838  wwlktovfo  14322  prmreclem2  16253  prdsval  16728  xpsfval  16839  xpssca  16849  xpsvsca  16850  isposix  17567  clatl  17726  ipoval  17764  mgm0b  17867  frmdval  18016  mgmnsgrpex  18096  sgrpnmndex  18097  symg2bas  18521  pmtrprfval  18615  pmtrprfvalrn  18616  psgnprfval1  18650  psgnprfval2  18651  isnzr2hash  20037  psgnghm  20724  psgnco  20727  evpmodpmf1o  20740  mdetralt  21217  m2detleiblem5  21234  m2detleiblem6  21235  m2detleiblem3  21238  m2detleiblem4  21239  m2detleib  21240  indistopon  21609  pptbas  21616  indistpsALT  21621  tuslem  22876  tmslem  23092  ehl2eudis  24025  sqff1o  25759  dchrval  25810  eengv  26765  structvtxvallem  26805  structiedg0val  26807  upgrbi  26878  umgrbi  26886  upgr1e  26898  umgredg  26923  uspgr1e  27026  usgr1e  27027  uspgr1ewop  27030  uspgr2v1e2w  27033  usgr2v1e2w  27034  usgrexmplef  27041  usgrexmpledg  27044  1loopgrnb0  27284  1egrvtxdg1  27291  1egrvtxdg0  27293  umgr2v2evtx  27303  umgr2v2eiedg  27305  umgr2v2e  27307  umgr2v2enb1  27308  umgr2v2evd2  27309  vdegp1ai  27318  vdegp1bi  27319  wlk2v2elem2  27935  wlk2v2e  27936  eupth2lems  28017  frcond2  28046  frcond3  28048  nfrgr2v  28051  frgr3vlem1  28052  frgr3vlem2  28053  frgrncvvdeqlem2  28079  ex-uni  28205  ex-eprel  28212  indf1ofs  31285  prsiga  31390  difelsiga  31392  inelpisys  31413  measssd  31474  carsgsigalem  31573  carsgclctun  31579  pmeasmono  31582  eulerpartlemn  31639  probun  31677  coinflipprob  31737  coinflipspace  31738  coinfliprv  31740  coinflippv  31741  cusgredgex  32368  subfacp1lem3  32429  subfacp1lem5  32431  ex-sategoelel12  32674  altopex  33421  altopthsn  33422  altxpsspw  33438  bj-endval  34599  poimirlem9  34916  poimirlem15  34922  tgrpset  37896  hlhilset  39085  kelac2lem  39684  kelac2  39685  mendval  39803  tr3dom  39914  fvrcllb0d  40058  fvrcllb0da  40059  fvrcllb1d  40060  corclrcl  40072  corcltrcl  40104  cotrclrcl  40107  clsk1indlem2  40412  clsk1indlem3  40413  clsk1indlem4  40414  clsk1indlem1  40415  mnuprdlem3  40630  mnurndlem1  40637  prsal  42623  sge0pr  42696  elsprel  43657  sprvalpw  43662  prprvalpw  43697  sbcpr  43703  nnsum3primes4  43973  nnsum3primesgbe  43977  strisomgrop  44025  mapprop  44414  zlmodzxzlmod  44422  zlmodzxzel  44423  zlmodzxz0  44424  zlmodzxzscm  44425  zlmodzxzadd  44426  zlmodzxzldeplem1  44575  zlmodzxzldeplem3  44577  zlmodzxzldeplem4  44578  ldepsnlinclem1  44580  ldepsnlinclem2  44581  ldepsnlinc  44583  prelrrx2  44720  rrx2xpref1o  44725  rrx2plordisom  44730  ehl2eudisval0  44732  rrx2linesl  44750  2sphere0  44757  line2  44759  line2x  44761  line2y  44762  onsetreclem1  44827