Theorem prex 5310

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 4669), 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 4636	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2815	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5308	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3471	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4635	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2815	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	syl5ib 247	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3487	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4667	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5309	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2839	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4668	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5309	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2839	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 187	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1543   ∈ wcel 2112  Vcvv 3398  {csn 4527  {cpr 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-sn 4528  df-pr 4530

This theorem is referenced by:  prelpw  5316  opex  5333  elopg  5335  opi2  5338  op1stb  5340  opth  5345  opeqsng  5371  opeqpr  5373  opthwiener  5382  uniop  5383  opthhausdorff  5385  opthhausdorff0  5386  fr2nr  5514  xpsspw  5664  relop  5704  f1prex  7072  unex  7509  tpex  7510  2oex  8197  pw2f1olem  8727  dif1en  8818  1sdom  8857  opthreg  9211  djuexALT  9503  pr2ne  9584  dfac2b  9709  intwun  10314  wunex2  10317  wuncval2  10326  intgru  10393  xrex  12548  seqexw  13555  pr2pwpr  14010  wwlktovfo  14490  prmreclem2  16433  prdsval  16914  xpsfval  17025  xpssca  17035  xpsvsca  17036  isposix  17786  clatl  17968  ipoval  17990  mgm0b  18083  frmdval  18232  mgmnsgrpex  18312  sgrpnmndex  18313  symg2bas  18739  pmtrprfval  18833  pmtrprfvalrn  18834  psgnprfval1  18868  psgnprfval2  18869  isnzr2hash  20256  psgnghm  20496  psgnco  20499  evpmodpmf1o  20512  mdetralt  21459  m2detleiblem5  21476  m2detleiblem6  21477  m2detleiblem3  21480  m2detleiblem4  21481  m2detleib  21482  indistopon  21852  pptbas  21859  indistpsALT  21864  tuslem  23118  tmslem  23334  ehl2eudis  24273  sqff1o  26018  dchrval  26069  eengv  27024  structvtxvallem  27065  structiedg0val  27067  upgrbi  27138  umgrbi  27146  upgr1e  27158  umgredg  27183  uspgr1e  27286  usgr1e  27287  uspgr1ewop  27290  uspgr2v1e2w  27293  usgr2v1e2w  27294  usgrexmplef  27301  usgrexmpledg  27304  1loopgrnb0  27544  1egrvtxdg1  27551  1egrvtxdg0  27553  umgr2v2evtx  27563  umgr2v2eiedg  27565  umgr2v2e  27567  umgr2v2enb1  27568  umgr2v2evd2  27569  vdegp1ai  27578  vdegp1bi  27579  wlk2v2elem2  28193  wlk2v2e  28194  eupth2lems  28275  frcond2  28304  frcond3  28306  nfrgr2v  28309  frgr3vlem1  28310  frgr3vlem2  28311  frgrncvvdeqlem2  28337  ex-uni  28463  ex-eprel  28470  idlsrgval  31316  indf1ofs  31660  prsiga  31765  difelsiga  31767  measssd  31849  carsgsigalem  31948  carsgclctun  31954  pmeasmono  31957  eulerpartlemn  32014  probun  32052  coinflipprob  32112  coinflipspace  32113  coinfliprv  32115  coinflippv  32116  cusgredgex  32750  subfacp1lem3  32811  subfacp1lem5  32813  ex-sategoelel12  33056  altopex  33948  altopthsn  33949  altxpsspw  33965  bj-endval  35169  poimirlem9  35472  poimirlem15  35478  tgrpset  38445  hlhilset  39634  kelac2lem  40533  kelac2  40534  mendval  40652  tr3dom  40761  fvrcllb0d  40919  fvrcllb0da  40920  fvrcllb1d  40921  corclrcl  40933  corcltrcl  40965  cotrclrcl  40968  clsk1indlem2  41270  clsk1indlem3  41271  clsk1indlem4  41272  clsk1indlem1  41273  mnuprdlem3  41506  mnurndlem1  41513  prsal  43477  sge0pr  43550  elsprel  44543  sprvalpw  44548  prprvalpw  44583  sbcpr  44589  nnsum3primes4  44856  nnsum3primesgbe  44860  strisomgrop  44908  fprmappr  45297  zlmodzxzlmod  45306  zlmodzxzel  45307  zlmodzxz0  45308  zlmodzxzscm  45309  zlmodzxzadd  45310  zlmodzxzldeplem1  45457  zlmodzxzldeplem3  45459  zlmodzxzldeplem4  45460  ldepsnlinclem1  45462  ldepsnlinclem2  45463  ldepsnlinc  45465  2arymaptfo  45616  prelrrx2  45675  rrx2xpref1o  45680  rrx2plordisom  45685  ehl2eudisval0  45687  rrx2linesl  45705  2sphere0  45712  line2  45714  line2x  45716  line2y  45717  onsetreclem1  46024