Theorem prex 5383

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 4725), 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 4692	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2822	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5379	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3512	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4691	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2822	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 244	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3511	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4723	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5382	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2845	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4724	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5382	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2845	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3441  {csn 4581  {cpr 4583

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-dif 3905  df-un 3907  df-nul 4287  df-sn 4582  df-pr 4584

This theorem is referenced by:  prelpw  5395  opex  5413  elopg  5415  opi2  5418  op1stb  5420  opth  5425  opeqsng  5452  opeqpr  5454  opthwiener  5463  uniop  5464  opthhausdorff  5466  opthhausdorff0  5467  fr2nr  5602  xpsspw  5759  relop  5800  f1prex  7232  unexg  7690  unexOLD  7692  tpex  7693  2oex  8410  en2prd  8988  pw2f1olem  9013  dif1en  9090  opthreg  9531  djuexALT  9838  dfac2b  10045  intwun  10650  wunex2  10653  wuncval2  10662  intgru  10729  xrex  12904  seqexw  13944  pr2pwpr  14406  wwlktovfo  14885  prmreclem2  16849  prdsval  17379  xpsfval  17491  xpssca  17501  xpsvsca  17502  isposix  18251  clatl  18435  ipoval  18457  mgm0b  18586  frmdval  18780  mgmnsgrpex  18860  sgrpnmndex  18861  symg2bas  19326  pmtrprfval  19420  pmtrprfvalrn  19421  psgnprfval1  19455  psgnprfval2  19456  isnzr2hash  20456  psgnghm  21539  psgnco  21542  evpmodpmf1o  21555  mdetralt  22556  m2detleiblem5  22573  m2detleiblem6  22574  m2detleiblem3  22577  m2detleiblem4  22578  m2detleib  22579  indistopon  22949  pptbas  22956  indistpsALT  22961  tuslem  24214  tmslem  24430  ehl2eudis  25382  sqff1o  27152  dchrval  27205  elno  27617  eengv  29035  structvtxvallem  29076  structiedg0val  29078  upgrbi  29149  umgrbi  29157  upgr1e  29169  umgredg  29194  uspgr1e  29300  usgr1e  29301  uspgr1ewop  29304  uspgr2v1e2w  29307  usgr2v1e2w  29308  usgrexmplef  29315  usgrexmpledg  29318  1loopgrnb0  29559  1egrvtxdg1  29566  1egrvtxdg0  29568  umgr2v2evtx  29578  umgr2v2eiedg  29580  umgr2v2e  29582  umgr2v2enb1  29583  umgr2v2evd2  29584  vdegp1ai  29593  vdegp1bi  29594  wlk2v2elem2  30214  wlk2v2e  30215  eupth2lems  30296  frcond2  30325  frcond3  30327  nfrgr2v  30330  frgr3vlem1  30331  frgr3vlem2  30332  frgrncvvdeqlem2  30358  ex-uni  30484  ex-eprel  30491  indf1ofs  32929  idlsrgval  33565  constr0  33875  prsiga  34269  difelsiga  34271  measssd  34353  carsgsigalem  34453  carsgclctun  34459  pmeasmono  34462  eulerpartlemn  34519  probun  34557  coinflipprob  34618  coinflipspace  34619  coinfliprv  34621  coinflippv  34622  cusgredgex  35297  subfacp1lem3  35357  subfacp1lem5  35359  ex-sategoelel12  35602  altopex  36135  altopthsn  36136  altxpsspw  36152  bj-endval  37491  poimirlem9  37801  poimirlem15  37807  tgrpset  41042  hlhilset  42231  aprilfools2025  42953  kelac2lem  43342  kelac2  43343  mendval  43457  tr3dom  43805  fvrcllb0d  43970  fvrcllb0da  43971  fvrcllb1d  43972  corclrcl  43984  corcltrcl  44016  cotrclrcl  44019  clsk1indlem2  44319  clsk1indlem3  44320  clsk1indlem4  44321  clsk1indlem1  44322  mnuprdlem3  44551  mnurndlem1  44558  permaxpr  45287  prsal  46598  sge0pr  46674  elsprel  47757  sprvalpw  47762  prprvalpw  47797  sbcpr  47803  nnsum3primes4  48070  nnsum3primesgbe  48074  opstrgric  48208  stgrfv  48235  stgredgel  48239  usgrexmpl1lem  48303  usgrexmpl1edg  48306  usgrexmpl1tri  48307  usgrexmpl2lem  48308  usgrexmpl2edg  48311  usgrexmpl2nb0  48313  usgrexmpl2nb1  48314  usgrexmpl2nb2  48315  usgrexmpl2nb3  48316  usgrexmpl2nb4  48317  usgrexmpl2nb5  48318  usgrexmpl2trifr  48319  gpgov  48324  gpgvtx  48325  gpgiedg  48326  gpgiedgdmellem  48328  gpgprismgr4cycllem2  48378  gpgprismgr4cycllem3  48379  gpgprismgr4cycllem8  48384  gpgprismgr4cycllem10  48386  pgnbgreunbgr  48407  fprmappr  48627  zlmodzxzlmod  48636  zlmodzxzel  48637  zlmodzxz0  48638  zlmodzxzscm  48639  zlmodzxzadd  48640  zlmodzxzldeplem1  48782  zlmodzxzldeplem3  48784  zlmodzxzldeplem4  48785  ldepsnlinclem1  48787  ldepsnlinclem2  48788  ldepsnlinc  48790  2arymaptfo  48936  prelrrx2  48995  rrx2xpref1o  49000  rrx2plordisom  49005  ehl2eudisval0  49007  rrx2linesl  49025  2sphere0  49032  line2  49034  line2x  49036  line2y  49037  resipos  49256  fucoppcffth  49692  termc2  49799  uobeqterm  49827  incat  49882  onsetreclem1  49986