Theorem prex 4836

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 4245), 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 4213	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2672	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 4834	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3239	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4212	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2672	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	syl5ib 233	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3252	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4243	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 4835	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	syl6eqel 2696	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4244	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 4835	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	syl6eqel 2696	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 177	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ∈ wcel 1977  Vcvv 3173  {csn 4125  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-un 3545  df-nul 3875  df-sn 4126  df-pr 4128

This theorem is referenced by:  prelpw  4841  opex  4859  elopg  4861  opi2  4865  op1stb  4867  opth  4871  opeqsn  4892  opeqpr  4893  propssopi  4896  opthwiener  4901  uniop  4902  fr2nr  5016  xpsspw  5156  relop  5194  f1prex  6439  unex  6854  tpex  6855  pw2f1olem  7949  1sdom  8048  opthreg  8398  pr2ne  8711  dfac2  8836  intwun  9436  wunex2  9439  wuncval2  9448  intgru  9515  xrex  11705  pr2pwpr  13116  wwlktovfo  13549  prmreclem2  15459  prdsval  15938  isposix  16780  clatl  16939  ipoval  16977  mgm0b  17079  frmdval  17211  mgmnsgrpex  17241  sgrpnmndex  17242  symg2bas  17641  pmtrprfval  17730  pmtrprfvalrn  17731  psgnprfval1  17765  psgnprfval2  17766  isnzr2hash  19085  psgnghm  19745  psgnco  19748  evpmodpmf1o  19761  mdetralt  20233  m2detleiblem5  20250  m2detleiblem6  20251  m2detleiblem3  20254  m2detleiblem4  20255  m2detleib  20256  indistopon  20615  pptbas  20622  indistpsALT  20627  tuslem  21881  tmslem  22097  sqff1o  24708  dchrval  24759  eengv  25659  structvtxvallem  25697  structiedg0val  25699  upgrbi  25760  umgrbi  25767  upgr1e  25779  edgastruct  25797  umgredg  25812  umgra1  25855  uslgra1  25901  usgra1  25902  usgraedgrnv  25906  usgrarnedg  25913  usgraedg4  25916  usgraexmplef  25929  usgraexmpledg  25932  cusgrarn  25988  wlkntrllem2  26090  wlkntrl  26092  constr1trl  26118  1pthon  26121  1pthon2v  26123  constr2trl  26129  constr2spth  26130  constr2pth  26131  2pthon  26132  2pthon3v  26134  usgra2adedgwlkon  26143  usg2wlk  26145  usg2wlkon  26146  constr3lem1  26173  constr3cyclpe  26191  3v3e3cycl2  26192  vdgr1b  26431  vdgr1a  26433  eupap1  26503  eupath2lem3  26506  eupath2  26507  vdegp1ai  26511  vdegp1bi  26512  frgraun  26523  frgra2v  26526  frgra3vlem1  26527  frgra3vlem2  26528  frgrancvvdeqlem3  26559  ex-uni  26675  ex-eprel  26682  indf1ofs  29415  prsiga  29521  difelsiga  29523  inelpisys  29544  measssd  29605  carsgsigalem  29704  carsgclctun  29710  pmeasmono  29713  eulerpartlemn  29770  probun  29808  coinflipprob  29868  coinflipspace  29869  coinfliprv  29871  coinflippv  29872  subfacp1lem3  30418  subfacp1lem5  30420  altopex  31237  altopthsn  31238  altxpsspw  31254  poimirlem9  32588  poimirlem15  32594  tgrpset  35051  hlhilset  36244  kelac2lem  36652  kelac2  36653  mendval  36772  fvrcllb0d  37004  fvrcllb0da  37005  fvrcllb1d  37006  corclrcl  37018  corcltrcl  37050  cotrclrcl  37053  clsk1indlem2  37360  clsk1indlem3  37361  clsk1indlem4  37362  clsk1indlem1  37363  prsal  39214  sge0pr  39287  nnsum3primes4  40204  nnsum3primesgbe  40208  uspgr1e  40470  usgr1e  40471  uspgr1ewop  40474  uspgr2v1e2w  40477  usgr2v1e2w  40478  usgrexmpledg  40486  1loopgrnb0  40717  1egrvtxdg1  40725  1egrvtxdg0  40727  umgr2v2evtx  40737  umgr2v2eiedg  40739  umgr2v2e  40741  umgr2v2enb1  40742  umgr2v2evd2  40743  vdegp1ai-av  40752  vdegp1bi-av  40753  1wlk2v2elem2  41323  1wlk2v2e  41324  eupth2lems  41406  frcond2  41439  nfrgr2v  41442  frgr3vlem1  41443  frgr3vlem2  41444  frgrncvvdeqlem3  41471  mapprop  41917  zlmodzxzlmod  41925  zlmodzxzel  41926  zlmodzxz0  41927  zlmodzxzscm  41928  zlmodzxzadd  41929  zlmodzxzldeplem1  42083  zlmodzxzldeplem3  42085  zlmodzxzldeplem4  42086  ldepsnlinclem1  42088  ldepsnlinclem2  42089  ldepsnlinc  42091  onsetreclem1  42247