Theorem prex 5350

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 4700), 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 4667	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2823	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5348	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3495	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4666	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2823	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	syl5ib 243	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3511	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4698	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5349	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2847	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4699	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5349	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2847	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422  {csn 4558  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-sn 4559  df-pr 4561

This theorem is referenced by:  prelpw  5356  opex  5373  elopg  5375  opi2  5378  op1stb  5380  opth  5385  opeqsng  5411  opeqpr  5413  opthwiener  5422  uniop  5423  opthhausdorff  5425  opthhausdorff0  5426  fr2nr  5558  xpsspw  5708  relop  5748  f1prex  7136  unex  7574  tpex  7575  2oex  8284  pw2f1olem  8816  dif1en  8907  1sdom  8955  opthreg  9306  djuexALT  9611  pr2ne  9692  dfac2b  9817  intwun  10422  wunex2  10425  wuncval2  10434  intgru  10501  xrex  12656  seqexw  13665  pr2pwpr  14121  wwlktovfo  14601  prmreclem2  16546  prdsval  17083  xpsfval  17194  xpssca  17204  xpsvsca  17205  isposix  17958  isposixOLD  17959  clatl  18141  ipoval  18163  mgm0b  18256  frmdval  18405  mgmnsgrpex  18485  sgrpnmndex  18486  symg2bas  18915  pmtrprfval  19010  pmtrprfvalrn  19011  psgnprfval1  19045  psgnprfval2  19046  isnzr2hash  20448  psgnghm  20697  psgnco  20700  evpmodpmf1o  20713  mdetralt  21665  m2detleiblem5  21682  m2detleiblem6  21683  m2detleiblem3  21686  m2detleiblem4  21687  m2detleib  21688  indistopon  22059  pptbas  22066  indistpsALT  22071  indistpsALTOLD  22072  tuslem  23326  tuslemOLD  23327  tmslem  23543  tmslemOLD  23544  ehl2eudis  24491  sqff1o  26236  dchrval  26287  eengv  27250  structvtxvallem  27293  structiedg0val  27295  upgrbi  27366  umgrbi  27374  upgr1e  27386  umgredg  27411  uspgr1e  27514  usgr1e  27515  uspgr1ewop  27518  uspgr2v1e2w  27521  usgr2v1e2w  27522  usgrexmplef  27529  usgrexmpledg  27532  1loopgrnb0  27772  1egrvtxdg1  27779  1egrvtxdg0  27781  umgr2v2evtx  27791  umgr2v2eiedg  27793  umgr2v2e  27795  umgr2v2enb1  27796  umgr2v2evd2  27797  vdegp1ai  27806  vdegp1bi  27807  wlk2v2elem2  28421  wlk2v2e  28422  eupth2lems  28503  frcond2  28532  frcond3  28534  nfrgr2v  28537  frgr3vlem1  28538  frgr3vlem2  28539  frgrncvvdeqlem2  28565  ex-uni  28691  ex-eprel  28698  idlsrgval  31550  indf1ofs  31894  prsiga  31999  difelsiga  32001  measssd  32083  carsgsigalem  32182  carsgclctun  32188  pmeasmono  32191  eulerpartlemn  32248  probun  32286  coinflipprob  32346  coinflipspace  32347  coinfliprv  32349  coinflippv  32350  cusgredgex  32983  subfacp1lem3  33044  subfacp1lem5  33046  ex-sategoelel12  33289  altopex  34189  altopthsn  34190  altxpsspw  34206  bj-endval  35413  poimirlem9  35713  poimirlem15  35719  tgrpset  38686  hlhilset  39875  kelac2lem  40805  kelac2  40806  mendval  40924  tr3dom  41033  fvrcllb0d  41190  fvrcllb0da  41191  fvrcllb1d  41192  corclrcl  41204  corcltrcl  41236  cotrclrcl  41239  clsk1indlem2  41541  clsk1indlem3  41542  clsk1indlem4  41543  clsk1indlem1  41544  mnuprdlem3  41781  mnurndlem1  41788  prsal  43749  sge0pr  43822  elsprel  44815  sprvalpw  44820  prprvalpw  44855  sbcpr  44861  nnsum3primes4  45128  nnsum3primesgbe  45132  strisomgrop  45180  fprmappr  45569  zlmodzxzlmod  45578  zlmodzxzel  45579  zlmodzxz0  45580  zlmodzxzscm  45581  zlmodzxzadd  45582  zlmodzxzldeplem1  45729  zlmodzxzldeplem3  45731  zlmodzxzldeplem4  45732  ldepsnlinclem1  45734  ldepsnlinclem2  45735  ldepsnlinc  45737  2arymaptfo  45888  prelrrx2  45947  rrx2xpref1o  45952  rrx2plordisom  45957  ehl2eudisval0  45959  rrx2linesl  45977  2sphere0  45984  line2  45986  line2x  45988  line2y  45989  onsetreclem1  46296