Theorem prex 4604

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 4056), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
prex	|- { A , B } e. _V

Proof of Theorem prex

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		preq2 4024	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2451	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4602	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 3092	. . . 4 |- ( B e. _V -> { x , B } e. _V )
5		preq1 4023	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2451	. . . 4 |- ( x = A -> ( { x , B } e. _V <-> { A , B } e. _V ) )
7	4, 6	syl5ib 219	. . 3 |- ( x = A -> ( B e. _V -> { A , B } e. _V ) )
8	7	vtocleg 3105	. 2 |- ( A e. _V -> ( B e. _V -> { A , B } e. _V ) )
9		prprc1 4054	. . 3 |- ( -. A e. _V -> { A , B } = { B } )
10		snex 4603	. . 3 |- { B } e. _V
11	9, 10	syl6eqel 2478	. 2 |- ( -. A e. _V -> { A , B } e. _V )
12		prprc2 4055	. . 3 |- ( -. B e. _V -> { A , B } = { A } )
13		snex 4603	. . 3 |- { A } e. _V
14	12, 13	syl6eqel 2478	. 2 |- ( -. B e. _V -> { A , B } e. _V )
15	8, 11, 14	pm2.61nii 166	1 |- { A , B } e. _V

Syntax hints:   -. wn 3   -> wi 4   = wceq 1399   e. wcel 1826   _Vcvv 3034   {csn 3944   {cpr 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-v 3036  df-dif 3392  df-un 3394  df-nul 3712  df-sn 3945  df-pr 3947

This theorem is referenced by:  prelpwi  4609  opex  4626  opi2  4630  op1stb  4632  opth  4636  opeqsn  4657  opeqpr  4658  opthwiener  4663  uniop  4664  fr2nr  4771  xpsspw  5029  relop  5066  unex  6497  tpex  6498  pw2f1olem  7540  1sdom  7639  opthreg  7949  pr2ne  8296  dfac2  8424  intwun  9024  wunex2  9027  wuncval2  9036  intgru  9103  xrex  11136  pr2pwpr  12424  wwlktovfo  12807  prmreclem2  14437  prdsval  14862  isposix  15704  clatl  15863  ipoval  15901  frmdval  16136  mgmnsgrpex  16166  sgrpnmndex  16167  symg2bas  16540  pmtrprfval  16629  pmtrprfvalrn  16630  psgnprfval1  16664  psgnprfval2  16665  isnzr2hash  18025  psgnghm  18707  psgnco  18710  evpmodpmf1o  18723  mdetralt  19195  m2detleiblem5  19212  m2detleiblem6  19213  m2detleiblem3  19216  m2detleiblem4  19217  m2detleib  19218  indistopon  19587  pptbas  19594  indistpsALT  19599  tuslem  20855  tmslem  21070  sqff1o  23573  dchrval  23626  eengv  24403  umgra1  24447  uslgra1  24493  usgra1  24494  usgraedgrnv  24498  usgrarnedg  24505  usgraedg4  24508  usgraexmpl  24522  usgraexmpledg  24524  cusgrarn  24580  wlkntrllem2  24683  wlkntrl  24685  constr1trl  24711  1pthon  24714  1pthon2v  24716  constr2trl  24722  constr2spth  24723  constr2pth  24724  2pthon  24725  2pthon3v  24727  usgra2adedgwlkon  24736  usg2wlk  24738  usg2wlkon  24739  constr3lem1  24766  constr3cyclpe  24784  3v3e3cycl2  24785  vdgr1b  25025  vdgr1a  25027  eupap1  25097  eupath2lem3  25100  eupath2  25101  vdegp1ai  25105  vdegp1bi  25106  frgraun  25117  frgra2v  25120  frgra3vlem1  25121  frgra3vlem2  25122  frgrancvvdeqlem3  25153  ex-uni  25268  ex-eprel  25275  indf1ofs  28174  prsiga  28280  difelsiga  28282  measssd  28342  carsgsigalem  28442  carsgclctun  28448  eulerpartlemn  28503  probun  28541  coinflipprob  28601  coinflipspace  28602  coinfliprv  28604  coinflippv  28605  subfacp1lem3  28815  subfacp1lem5  28817  altopex  29763  altopthsn  29764  altxpsspw  29780  kelac2lem  31176  kelac2  31177  mendval  31300  prelpw  32620  mapprop  33135  zlmodzxzlmod  33143  zlmodzxzel  33144  zlmodzxz0  33145  zlmodzxzscm  33146  zlmodzxzadd  33147  zlmodzxzldeplem1  33301  zlmodzxzldeplem3  33303  zlmodzxzldeplem4  33304  ldepsnlinclem1  33306  ldepsnlinclem2  33307  ldepsnlinc  33309  bj-elopg  34950  tgrpset  36884  hlhilset  38077  corclrcl  38248  corcltrcl  38249  cotrclrcl  38250