Theorem prex 5452

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 4792), 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 4759	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2829	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5448	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3566	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4758	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2829	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 244	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3565	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4790	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5451	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2852	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4791	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5451	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2852	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2108  Vcvv 3488  {csn 4648  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353  df-sn 4649  df-pr 4651

This theorem is referenced by:  prelpw  5466  opex  5484  elopg  5486  opi2  5489  op1stb  5491  opth  5496  opeqsng  5522  opeqpr  5524  opthwiener  5533  uniop  5534  opthhausdorff  5536  opthhausdorff0  5537  fr2nr  5677  xpsspw  5833  relop  5875  f1prex  7320  unexg  7778  unexOLD  7780  tpex  7781  2oex  8533  en2prd  9114  pw2f1olem  9142  dif1en  9226  dif1enOLD  9228  1sdomOLD  9312  opthreg  9687  djuexALT  9991  pr2neOLD  10074  dfac2b  10200  intwun  10804  wunex2  10807  wuncval2  10816  intgru  10883  xrex  13052  seqexw  14068  pr2pwpr  14528  wwlktovfo  15007  prmreclem2  16964  prdsval  17515  xpsfval  17626  xpssca  17636  xpsvsca  17637  isposix  18395  isposixOLD  18396  clatl  18578  ipoval  18600  mgm0b  18695  frmdval  18886  mgmnsgrpex  18966  sgrpnmndex  18967  symg2bas  19434  pmtrprfval  19529  pmtrprfvalrn  19530  psgnprfval1  19564  psgnprfval2  19565  isnzr2hash  20545  psgnghm  21621  psgnco  21624  evpmodpmf1o  21637  mdetralt  22635  m2detleiblem5  22652  m2detleiblem6  22653  m2detleiblem3  22656  m2detleiblem4  22657  m2detleib  22658  indistopon  23029  pptbas  23036  indistpsALT  23041  indistpsALTOLD  23042  tuslem  24296  tuslemOLD  24297  tmslem  24515  tmslemOLD  24516  ehl2eudis  25475  sqff1o  27243  dchrval  27296  elno  27708  eengv  29012  structvtxvallem  29055  structiedg0val  29057  upgrbi  29128  umgrbi  29136  upgr1e  29148  umgredg  29173  uspgr1e  29279  usgr1e  29280  uspgr1ewop  29283  uspgr2v1e2w  29286  usgr2v1e2w  29287  usgrexmplef  29294  usgrexmpledg  29297  1loopgrnb0  29538  1egrvtxdg1  29545  1egrvtxdg0  29547  umgr2v2evtx  29557  umgr2v2eiedg  29559  umgr2v2e  29561  umgr2v2enb1  29562  umgr2v2evd2  29563  vdegp1ai  29572  vdegp1bi  29573  wlk2v2elem2  30188  wlk2v2e  30189  eupth2lems  30270  frcond2  30299  frcond3  30301  nfrgr2v  30304  frgr3vlem1  30305  frgr3vlem2  30306  frgrncvvdeqlem2  30332  ex-uni  30458  ex-eprel  30465  idlsrgval  33496  constr0  33727  indf1ofs  33990  prsiga  34095  difelsiga  34097  measssd  34179  carsgsigalem  34280  carsgclctun  34286  pmeasmono  34289  eulerpartlemn  34346  probun  34384  coinflipprob  34444  coinflipspace  34445  coinfliprv  34447  coinflippv  34448  cusgredgex  35089  subfacp1lem3  35150  subfacp1lem5  35152  ex-sategoelel12  35395  altopex  35924  altopthsn  35925  altxpsspw  35941  bj-endval  37281  poimirlem9  37589  poimirlem15  37595  tgrpset  40702  hlhilset  41891  aprilfools2025  42629  kelac2lem  43021  kelac2  43022  mendval  43140  tr3dom  43490  fvrcllb0d  43655  fvrcllb0da  43656  fvrcllb1d  43657  corclrcl  43669  corcltrcl  43701  cotrclrcl  43704  clsk1indlem2  44004  clsk1indlem3  44005  clsk1indlem4  44006  clsk1indlem1  44007  mnuprdlem3  44243  mnurndlem1  44250  prsal  46239  sge0pr  46315  elsprel  47349  sprvalpw  47354  prprvalpw  47389  sbcpr  47395  nnsum3primes4  47662  nnsum3primesgbe  47666  opstrgric  47779  usgrexmpl1lem  47836  usgrexmpl1edg  47839  usgrexmpl1tri  47840  usgrexmpl2lem  47841  usgrexmpl2edg  47844  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  fprmappr  48070  zlmodzxzlmod  48079  zlmodzxzel  48080  zlmodzxz0  48081  zlmodzxzscm  48082  zlmodzxzadd  48083  zlmodzxzldeplem1  48229  zlmodzxzldeplem3  48231  zlmodzxzldeplem4  48232  ldepsnlinclem1  48234  ldepsnlinclem2  48235  ldepsnlinc  48237  2arymaptfo  48388  prelrrx2  48447  rrx2xpref1o  48452  rrx2plordisom  48457  ehl2eudisval0  48459  rrx2linesl  48477  2sphere0  48484  line2  48486  line2x  48488  line2y  48489  onsetreclem1  48797