Theorem prex 4689

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 4139), 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 4107	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2536	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4687	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 3171	. . . 4 |- ( B e. _V -> { x , B } e. _V )
5		preq1 4106	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2536	. . . 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 3184	. 2 |- ( A e. _V -> ( B e. _V -> { A , B } e. _V ) )
9		prprc1 4137	. . 3 |- ( -. A e. _V -> { A , B } = { B } )
10		snex 4688	. . 3 |- { B } e. _V
11	9, 10	syl6eqel 2563	. 2 |- ( -. A e. _V -> { A , B } e. _V )
12		prprc2 4138	. . 3 |- ( -. B e. _V -> { A , B } = { A } )
13		snex 4688	. . 3 |- { A } e. _V
14	12, 13	syl6eqel 2563	. 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 1379   e. wcel 1767   _Vcvv 3113   {csn 4027   {cpr 4029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-un 3481  df-nul 3786  df-sn 4028  df-pr 4030

This theorem is referenced by:  prelpwi  4694  opex  4711  opi2  4715  op1stb  4717  opth  4721  opeqsn  4743  opeqpr  4744  opthwiener  4749  uniop  4750  fr2nr  4857  xpsspwOLD  5115  relop  5151  unex  6580  tpex  6581  pw2f1olem  7618  1sdom  7719  opthreg  8031  pr2ne  8379  dfac2  8507  intwun  9109  wunex2  9112  wuncval2  9121  intgru  9188  xrex  11213  pr2pwpr  12482  wwlktovfo  12855  prmreclem2  14290  prdsval  14706  isposix  15440  clatl  15599  ipoval  15637  frmdval  15842  symg2bas  16218  pmtrprfval  16308  pmtrprfvalrn  16309  psgnprfval1  16343  psgnprfval2  16344  psgnghm  18383  psgnco  18386  evpmodpmf1o  18399  mdetralt  18877  m2detleiblem5  18894  m2detleiblem6  18895  m2detleiblem3  18898  m2detleiblem4  18899  m2detleib  18900  indistopon  19268  pptbas  19275  indistpsALT  19280  tuslem  20505  tmslem  20720  sqff1o  23184  dchrval  23237  eengv  23958  umgra1  24002  uslgra1  24048  usgra1  24049  usgraedgrnv  24053  usgrarnedg  24060  usgraedg4  24063  usgraexmpl  24077  usgraexmpledg  24079  cusgrarn  24135  wlkntrllem2  24238  wlkntrl  24240  constr1trl  24266  1pthon  24269  1pthon2v  24271  constr2wlk  24276  constr2trl  24277  constr2spth  24278  constr2pth  24279  2pthon  24280  2pthon3v  24282  usgra2adedgwlkon  24291  usg2wlk  24293  usg2wlkon  24294  constr3lem1  24321  constr3cyclpe  24339  3v3e3cycl2  24340  vdgr1b  24580  vdgr1a  24582  eupap1  24652  eupath2lem3  24655  eupath2  24656  vdegp1ai  24660  vdegp1bi  24661  frgraun  24672  frgra2v  24675  frgra3vlem1  24676  frgra3vlem2  24677  frgrancvvdeqlem3  24709  ex-uni  24824  ex-eprel  24831  indf1ofs  27679  prsiga  27771  difelsiga  27773  measssd  27826  eulerpartlemn  27960  probun  27998  coinflipprob  28058  coinflipspace  28059  coinfliprv  28061  subfacp1lem3  28266  subfacp1lem5  28268  altopex  29187  altopthsn  29188  altxpsspw  29204  kelac2lem  30614  kelac2  30615  mendval  30737  prelpw  31766  mapprop  31999  zlmodzxzlmod  32007  zlmodzxzel  32008  zlmodzxz0  32009  zlmodzxzscm  32010  zlmodzxzadd  32011  isnzr2hash  32027  zlmodzxzldeplem1  32182  zlmodzxzldeplem3  32184  zlmodzxzldeplem4  32185  ldepsnlinclem1  32187  ldepsnlinclem2  32188  ldepsnlinc  32190  bj-elopg  33674  tgrpset  35541  hlhilset  36734