Theorem prex 5392

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 4731), 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 4698	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2813	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5388	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3520	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4697	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2813	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 244	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3519	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4729	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5391	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2836	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4730	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5391	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2836	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447  {csn 4589  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-un 3919  df-nul 4297  df-sn 4590  df-pr 4592

This theorem is referenced by:  prelpw  5406  opex  5424  elopg  5426  opi2  5429  op1stb  5431  opth  5436  opeqsng  5463  opeqpr  5465  opthwiener  5474  uniop  5475  opthhausdorff  5477  opthhausdorff0  5478  fr2nr  5615  xpsspw  5772  relop  5814  f1prex  7259  unexg  7719  unexOLD  7721  tpex  7722  2oex  8445  en2prd  9019  pw2f1olem  9045  dif1en  9124  dif1enOLD  9126  1sdomOLD  9196  opthreg  9571  djuexALT  9875  pr2neOLD  9958  dfac2b  10084  intwun  10688  wunex2  10691  wuncval2  10700  intgru  10767  xrex  12946  seqexw  13982  pr2pwpr  14444  wwlktovfo  14924  prmreclem2  16888  prdsval  17418  xpsfval  17529  xpssca  17539  xpsvsca  17540  isposix  18285  clatl  18467  ipoval  18489  mgm0b  18584  frmdval  18778  mgmnsgrpex  18858  sgrpnmndex  18859  symg2bas  19323  pmtrprfval  19417  pmtrprfvalrn  19418  psgnprfval1  19452  psgnprfval2  19453  isnzr2hash  20428  psgnghm  21489  psgnco  21492  evpmodpmf1o  21505  mdetralt  22495  m2detleiblem5  22512  m2detleiblem6  22513  m2detleiblem3  22516  m2detleiblem4  22517  m2detleib  22518  indistopon  22888  pptbas  22895  indistpsALT  22900  tuslem  24154  tmslem  24370  ehl2eudis  25322  sqff1o  27092  dchrval  27145  elno  27557  eengv  28906  structvtxvallem  28947  structiedg0val  28949  upgrbi  29020  umgrbi  29028  upgr1e  29040  umgredg  29065  uspgr1e  29171  usgr1e  29172  uspgr1ewop  29175  uspgr2v1e2w  29178  usgr2v1e2w  29179  usgrexmplef  29186  usgrexmpledg  29189  1loopgrnb0  29430  1egrvtxdg1  29437  1egrvtxdg0  29439  umgr2v2evtx  29449  umgr2v2eiedg  29451  umgr2v2e  29453  umgr2v2enb1  29454  umgr2v2evd2  29455  vdegp1ai  29464  vdegp1bi  29465  wlk2v2elem2  30085  wlk2v2e  30086  eupth2lems  30167  frcond2  30196  frcond3  30198  nfrgr2v  30201  frgr3vlem1  30202  frgr3vlem2  30203  frgrncvvdeqlem2  30229  ex-uni  30355  ex-eprel  30362  indf1ofs  32789  idlsrgval  33474  constr0  33727  prsiga  34121  difelsiga  34123  measssd  34205  carsgsigalem  34306  carsgclctun  34312  pmeasmono  34315  eulerpartlemn  34372  probun  34410  coinflipprob  34471  coinflipspace  34472  coinfliprv  34474  coinflippv  34475  cusgredgex  35109  subfacp1lem3  35169  subfacp1lem5  35171  ex-sategoelel12  35414  altopex  35948  altopthsn  35949  altxpsspw  35965  bj-endval  37303  poimirlem9  37623  poimirlem15  37629  tgrpset  40739  hlhilset  41928  aprilfools2025  42662  kelac2lem  43053  kelac2  43054  mendval  43168  tr3dom  43517  fvrcllb0d  43682  fvrcllb0da  43683  fvrcllb1d  43684  corclrcl  43696  corcltrcl  43728  cotrclrcl  43731  clsk1indlem2  44031  clsk1indlem3  44032  clsk1indlem4  44033  clsk1indlem1  44034  mnuprdlem3  44263  mnurndlem1  44270  permaxpr  45000  prsal  46316  sge0pr  46392  elsprel  47476  sprvalpw  47481  prprvalpw  47516  sbcpr  47522  nnsum3primes4  47789  nnsum3primesgbe  47793  opstrgric  47926  stgrfv  47952  stgredgel  47956  usgrexmpl1lem  48012  usgrexmpl1edg  48015  usgrexmpl1tri  48016  usgrexmpl2lem  48017  usgrexmpl2edg  48020  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  gpgov  48033  gpgvtx  48034  gpgiedg  48035  gpgiedgdmellem  48037  gpgprismgr4cycllem2  48086  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem8  48092  gpgprismgr4cycllem10  48094  pgnbgreunbgr  48115  fprmappr  48333  zlmodzxzlmod  48342  zlmodzxzel  48343  zlmodzxz0  48344  zlmodzxzscm  48345  zlmodzxzadd  48346  zlmodzxzldeplem1  48489  zlmodzxzldeplem3  48491  zlmodzxzldeplem4  48492  ldepsnlinclem1  48494  ldepsnlinclem2  48495  ldepsnlinc  48497  2arymaptfo  48643  prelrrx2  48702  rrx2xpref1o  48707  rrx2plordisom  48712  ehl2eudisval0  48714  rrx2linesl  48732  2sphere0  48739  line2  48741  line2x  48743  line2y  48744  resipos  48963  fucoppcffth  49400  termc2  49507  uobeqterm  49535  incat  49590  onsetreclem1  49694