Theorem prex 5394

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 4733), 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 4700	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2817	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5390	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3526	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4699	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2817	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 243	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3515	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4731	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5393	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2840	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4732	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5393	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2840	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3446  {csn 4591  {cpr 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916  df-un 3918  df-nul 4288  df-sn 4592  df-pr 4594

This theorem is referenced by:  prelpw  5408  opex  5426  elopg  5428  opi2  5431  op1stb  5433  opth  5438  opeqsng  5465  opeqpr  5467  opthwiener  5476  uniop  5477  opthhausdorff  5479  opthhausdorff0  5480  fr2nr  5616  xpsspw  5770  relop  5811  f1prex  7235  unex  7685  tpex  7686  2oex  8428  en2prd  8999  pw2f1olem  9027  dif1en  9111  dif1enOLD  9113  1sdomOLD  9200  opthreg  9563  djuexALT  9867  pr2neOLD  9950  dfac2b  10075  intwun  10680  wunex2  10683  wuncval2  10692  intgru  10759  xrex  12921  seqexw  13932  pr2pwpr  14390  wwlktovfo  14859  prmreclem2  16800  prdsval  17351  xpsfval  17462  xpssca  17472  xpsvsca  17473  isposix  18228  isposixOLD  18229  clatl  18411  ipoval  18433  mgm0b  18526  frmdval  18675  mgmnsgrpex  18755  sgrpnmndex  18756  symg2bas  19188  pmtrprfval  19283  pmtrprfvalrn  19284  psgnprfval1  19318  psgnprfval2  19319  isnzr2hash  20208  psgnghm  21021  psgnco  21024  evpmodpmf1o  21037  mdetralt  21994  m2detleiblem5  22011  m2detleiblem6  22012  m2detleiblem3  22015  m2detleiblem4  22016  m2detleib  22017  indistopon  22388  pptbas  22395  indistpsALT  22400  indistpsALTOLD  22401  tuslem  23655  tuslemOLD  23656  tmslem  23874  tmslemOLD  23875  ehl2eudis  24823  sqff1o  26568  dchrval  26619  eengv  27991  structvtxvallem  28034  structiedg0val  28036  upgrbi  28107  umgrbi  28115  upgr1e  28127  umgredg  28152  uspgr1e  28255  usgr1e  28256  uspgr1ewop  28259  uspgr2v1e2w  28262  usgr2v1e2w  28263  usgrexmplef  28270  usgrexmpledg  28273  1loopgrnb0  28513  1egrvtxdg1  28520  1egrvtxdg0  28522  umgr2v2evtx  28532  umgr2v2eiedg  28534  umgr2v2e  28536  umgr2v2enb1  28537  umgr2v2evd2  28538  vdegp1ai  28547  vdegp1bi  28548  wlk2v2elem2  29163  wlk2v2e  29164  eupth2lems  29245  frcond2  29274  frcond3  29276  nfrgr2v  29279  frgr3vlem1  29280  frgr3vlem2  29281  frgrncvvdeqlem2  29307  ex-uni  29433  ex-eprel  29440  idlsrgval  32321  indf1ofs  32714  prsiga  32819  difelsiga  32821  measssd  32903  carsgsigalem  33004  carsgclctun  33010  pmeasmono  33013  eulerpartlemn  33070  probun  33108  coinflipprob  33168  coinflipspace  33169  coinfliprv  33171  coinflippv  33172  cusgredgex  33802  subfacp1lem3  33863  subfacp1lem5  33865  ex-sategoelel12  34108  altopex  34621  altopthsn  34622  altxpsspw  34638  bj-endval  35859  poimirlem9  36160  poimirlem15  36166  tgrpset  39281  hlhilset  40470  kelac2lem  41449  kelac2  41450  mendval  41568  tr3dom  41922  fvrcllb0d  42087  fvrcllb0da  42088  fvrcllb1d  42089  corclrcl  42101  corcltrcl  42133  cotrclrcl  42136  clsk1indlem2  42436  clsk1indlem3  42437  clsk1indlem4  42438  clsk1indlem1  42439  mnuprdlem3  42676  mnurndlem1  42683  prsal  44679  sge0pr  44755  elsprel  45787  sprvalpw  45792  prprvalpw  45827  sbcpr  45833  nnsum3primes4  46100  nnsum3primesgbe  46104  strisomgrop  46152  fprmappr  46541  zlmodzxzlmod  46550  zlmodzxzel  46551  zlmodzxz0  46552  zlmodzxzscm  46553  zlmodzxzadd  46554  zlmodzxzldeplem1  46701  zlmodzxzldeplem3  46703  zlmodzxzldeplem4  46704  ldepsnlinclem1  46706  ldepsnlinclem2  46707  ldepsnlinc  46709  2arymaptfo  46860  prelrrx2  46919  rrx2xpref1o  46924  rrx2plordisom  46929  ehl2eudisval0  46931  rrx2linesl  46949  2sphere0  46956  line2  46958  line2x  46960  line2y  46961  onsetreclem1  47270