Theorem prex 5382

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440  {csn 4580  {cpr 4582

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286  df-sn 4581  df-pr 4583

This theorem is referenced by:  prelpw  5394  opex  5412  elopg  5414  opi2  5417  op1stb  5419  opth  5424  opeqsng  5451  opeqpr  5453  opthwiener  5462  uniop  5463  opthhausdorff  5465  opthhausdorff0  5466  fr2nr  5601  xpsspw  5758  relop  5799  f1prex  7230  unexg  7688  unexOLD  7690  tpex  7691  2oex  8408  en2prd  8984  pw2f1olem  9009  dif1en  9086  opthreg  9527  djuexALT  9834  dfac2b  10041  intwun  10646  wunex2  10649  wuncval2  10658  intgru  10725  xrex  12900  seqexw  13940  pr2pwpr  14402  wwlktovfo  14881  prmreclem2  16845  prdsval  17375  xpsfval  17487  xpssca  17497  xpsvsca  17498  isposix  18247  clatl  18431  ipoval  18453  mgm0b  18582  frmdval  18776  mgmnsgrpex  18856  sgrpnmndex  18857  symg2bas  19322  pmtrprfval  19416  pmtrprfvalrn  19417  psgnprfval1  19451  psgnprfval2  19452  isnzr2hash  20452  psgnghm  21535  psgnco  21538  evpmodpmf1o  21551  mdetralt  22552  m2detleiblem5  22569  m2detleiblem6  22570  m2detleiblem3  22573  m2detleiblem4  22574  m2detleib  22575  indistopon  22945  pptbas  22952  indistpsALT  22957  tuslem  24210  tmslem  24426  ehl2eudis  25378  sqff1o  27148  dchrval  27201  elno  27613  eengv  29052  structvtxvallem  29093  structiedg0val  29095  upgrbi  29166  umgrbi  29174  upgr1e  29186  umgredg  29211  uspgr1e  29317  usgr1e  29318  uspgr1ewop  29321  uspgr2v1e2w  29324  usgr2v1e2w  29325  usgrexmplef  29332  usgrexmpledg  29335  1loopgrnb0  29576  1egrvtxdg1  29583  1egrvtxdg0  29585  umgr2v2evtx  29595  umgr2v2eiedg  29597  umgr2v2e  29599  umgr2v2enb1  29600  umgr2v2evd2  29601  vdegp1ai  29610  vdegp1bi  29611  wlk2v2elem2  30231  wlk2v2e  30232  eupth2lems  30313  frcond2  30342  frcond3  30344  nfrgr2v  30347  frgr3vlem1  30348  frgr3vlem2  30349  frgrncvvdeqlem2  30375  ex-uni  30501  ex-eprel  30508  indf1ofs  32948  idlsrgval  33584  constr0  33894  prsiga  34288  difelsiga  34290  measssd  34372  carsgsigalem  34472  carsgclctun  34478  pmeasmono  34481  eulerpartlemn  34538  probun  34576  coinflipprob  34637  coinflipspace  34638  coinfliprv  34640  coinflippv  34641  cusgredgex  35316  subfacp1lem3  35376  subfacp1lem5  35378  ex-sategoelel12  35621  altopex  36154  altopthsn  36155  altxpsspw  36171  bj-endval  37516  poimirlem9  37826  poimirlem15  37832  tgrpset  41001  hlhilset  42190  aprilfools2025  42913  kelac2lem  43302  kelac2  43303  mendval  43417  tr3dom  43765  fvrcllb0d  43930  fvrcllb0da  43931  fvrcllb1d  43932  corclrcl  43944  corcltrcl  43976  cotrclrcl  43979  clsk1indlem2  44279  clsk1indlem3  44280  clsk1indlem4  44281  clsk1indlem1  44282  mnuprdlem3  44511  mnurndlem1  44518  permaxpr  45247  prsal  46558  sge0pr  46634  elsprel  47717  sprvalpw  47722  prprvalpw  47757  sbcpr  47763  nnsum3primes4  48030  nnsum3primesgbe  48034  opstrgric  48168  stgrfv  48195  stgredgel  48199  usgrexmpl1lem  48263  usgrexmpl1edg  48266  usgrexmpl1tri  48267  usgrexmpl2lem  48268  usgrexmpl2edg  48271  usgrexmpl2nb0  48273  usgrexmpl2nb1  48274  usgrexmpl2nb2  48275  usgrexmpl2nb3  48276  usgrexmpl2nb4  48277  usgrexmpl2nb5  48278  usgrexmpl2trifr  48279  gpgov  48284  gpgvtx  48285  gpgiedg  48286  gpgiedgdmellem  48288  gpgprismgr4cycllem2  48338  gpgprismgr4cycllem3  48339  gpgprismgr4cycllem8  48344  gpgprismgr4cycllem10  48346  pgnbgreunbgr  48367  fprmappr  48587  zlmodzxzlmod  48596  zlmodzxzel  48597  zlmodzxz0  48598  zlmodzxzscm  48599  zlmodzxzadd  48600  zlmodzxzldeplem1  48742  zlmodzxzldeplem3  48744  zlmodzxzldeplem4  48745  ldepsnlinclem1  48747  ldepsnlinclem2  48748  ldepsnlinc  48750  2arymaptfo  48896  prelrrx2  48955  rrx2xpref1o  48960  rrx2plordisom  48965  ehl2eudisval0  48967  rrx2linesl  48985  2sphere0  48992  line2  48994  line2x  48996  line2y  48997  resipos  49216  fucoppcffth  49652  termc2  49759  uobeqterm  49787  incat  49842  onsetreclem1  49946