Theorem prex 4656

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 4097), 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 4065	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2524	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4654	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 3119	. . . 4 |- ( B e. _V -> { x , B } e. _V )
5		preq1 4064	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2524	. . . 4 |- ( x = A -> ( { x , B } e. _V <-> { A , B } e. _V ) )
7	4, 6	syl5ib 227	. . 3 |- ( x = A -> ( B e. _V -> { A , B } e. _V ) )
8	7	vtocleg 3132	. 2 |- ( A e. _V -> ( B e. _V -> { A , B } e. _V ) )
9		prprc1 4095	. . 3 |- ( -. A e. _V -> { A , B } = { B } )
10		snex 4655	. . 3 |- { B } e. _V
11	9, 10	syl6eqel 2548	. 2 |- ( -. A e. _V -> { A , B } e. _V )
12		prprc2 4096	. . 3 |- ( -. B e. _V -> { A , B } = { A } )
13		snex 4655	. . 3 |- { A } e. _V
14	12, 13	syl6eqel 2548	. 2 |- ( -. B e. _V -> { A , B } e. _V )
15	8, 11, 14	pm2.61nii 171	1 |- { A , B } e. _V

Syntax hints:   -. wn 3   -> wi 4   = wceq 1455   e. wcel 1898   _Vcvv 3057   {csn 3980   {cpr 3982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-v 3059  df-dif 3419  df-un 3421  df-nul 3744  df-sn 3981  df-pr 3983

This theorem is referenced by:  prelpwi  4661  opex  4678  elopg  4680  opi2  4684  op1stb  4686  opth  4690  opeqsn  4711  opeqpr  4712  opthwiener  4717  uniop  4718  fr2nr  4831  xpsspw  4967  relop  5004  f1prex  6207  unex  6616  tpex  6617  pw2f1olem  7702  1sdom  7801  opthreg  8149  pr2ne  8462  dfac2  8587  intwun  9186  wunex2  9189  wuncval2  9198  intgru  9265  xrex  11328  pr2pwpr  12669  wwlktovfo  13082  prmreclem2  14910  prdsval  15402  isposix  16252  clatl  16411  ipoval  16449  frmdval  16684  mgmnsgrpex  16714  sgrpnmndex  16715  symg2bas  17088  pmtrprfval  17177  pmtrprfvalrn  17178  psgnprfval1  17212  psgnprfval2  17213  isnzr2hash  18537  psgnghm  19197  psgnco  19200  evpmodpmf1o  19213  mdetralt  19682  m2detleiblem5  19699  m2detleiblem6  19700  m2detleiblem3  19703  m2detleiblem4  19704  m2detleib  19705  indistopon  20065  pptbas  20072  indistpsALT  20077  tuslem  21331  tmslem  21546  sqff1o  24158  dchrval  24211  eengv  25058  umgra1  25102  uslgra1  25148  usgra1  25149  usgraedgrnv  25153  usgrarnedg  25160  usgraedg4  25163  usgraexmplef  25177  usgraexmpledg  25180  cusgrarn  25236  wlkntrllem2  25339  wlkntrl  25341  constr1trl  25367  1pthon  25370  1pthon2v  25372  constr2trl  25378  constr2spth  25379  constr2pth  25380  2pthon  25381  2pthon3v  25383  usgra2adedgwlkon  25392  usg2wlk  25394  usg2wlkon  25395  constr3lem1  25422  constr3cyclpe  25440  3v3e3cycl2  25441  vdgr1b  25681  vdgr1a  25683  eupap1  25753  eupath2lem3  25756  eupath2  25757  vdegp1ai  25761  vdegp1bi  25762  frgraun  25773  frgra2v  25776  frgra3vlem1  25777  frgra3vlem2  25778  frgrancvvdeqlem3  25809  ex-uni  25925  ex-eprel  25932  indf1ofs  28896  prsiga  29002  difelsiga  29004  inelpisys  29025  measssd  29086  carsgsigalem  29196  carsgclctun  29202  pmeasmono  29206  eulerpartlemn  29263  probun  29301  coinflipprob  29361  coinflipspace  29362  coinfliprv  29364  coinflippv  29365  subfacp1lem3  29954  subfacp1lem5  29956  altopex  30776  altopthsn  30777  altxpsspw  30793  poimirlem9  31994  poimirlem15  32000  tgrpset  34357  hlhilset  35550  kelac2lem  35967  kelac2  35968  mendval  36094  fvrcllb0d  36330  fvrcllb0da  36331  fvrcllb1d  36332  corclrcl  36344  corcltrcl  36376  cotrclrcl  36379  prsal  38217  sge0pr  38274  nnsum3primes4  38921  nnsum3primesgbe  38925  prelpw  39033  propssopi  39040  structvtxvallem  39168  structiedg0val  39170  upgr1e  39249  edgastruct  39263  umgredg  39277  uspgr1e  39369  usgr1e  39370  uspgr1ewop  39373  uspgr2v1e2w  39376  usgr2v1e2w  39377  usgrexmpledg  39384  uspgrloopnb0  39606  umgr2v2evtx  39608  umgr2v2eiedg  39610  umgr2v2e  39612  umgr2v2enb1  39613  umgr2v2evd2  39614  1wlk2v2elem2  39871  1wlk2v2e  39872  mapprop  40400  zlmodzxzlmod  40408  zlmodzxzel  40409  zlmodzxz0  40410  zlmodzxzscm  40411  zlmodzxzadd  40412  zlmodzxzldeplem1  40566  zlmodzxzldeplem3  40568  zlmodzxzldeplem4  40569  ldepsnlinclem1  40571  ldepsnlinclem2  40572  ldepsnlinc  40574