Theorem prex 4675

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 4123), 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 4091	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2510	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4673	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 3151	. . . 4 |- ( B e. _V -> { x , B } e. _V )
5		preq1 4090	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2510	. . . 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 3164	. 2 |- ( A e. _V -> ( B e. _V -> { A , B } e. _V ) )
9		prprc1 4121	. . 3 |- ( -. A e. _V -> { A , B } = { B } )
10		snex 4674	. . 3 |- { B } e. _V
11	9, 10	syl6eqel 2537	. 2 |- ( -. A e. _V -> { A , B } e. _V )
12		prprc2 4122	. . 3 |- ( -. B e. _V -> { A , B } = { A } )
13		snex 4674	. . 3 |- { A } e. _V
14	12, 13	syl6eqel 2537	. 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 1381   e. wcel 1802   _Vcvv 3093   {csn 4010   {cpr 4012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-v 3095  df-dif 3461  df-un 3463  df-nul 3768  df-sn 4011  df-pr 4013

This theorem is referenced by:  prelpwi  4680  opex  4697  opi2  4701  op1stb  4703  opth  4707  opeqsn  4729  opeqpr  4730  opthwiener  4735  uniop  4736  fr2nr  4843  xpsspwOLD  5103  relop  5139  unex  6579  tpex  6580  pw2f1olem  7619  1sdom  7720  opthreg  8033  pr2ne  8381  dfac2  8509  intwun  9111  wunex2  9114  wuncval2  9123  intgru  9190  xrex  11221  pr2pwpr  12494  wwlktovfo  12870  prmreclem2  14307  prdsval  14724  isposix  15456  clatl  15615  ipoval  15653  frmdval  15888  mgmnsgrpex  15918  sgrpnmndex  15919  symg2bas  16292  pmtrprfval  16381  pmtrprfvalrn  16382  psgnprfval1  16416  psgnprfval2  16417  isnzr2hash  17780  psgnghm  18483  psgnco  18486  evpmodpmf1o  18499  mdetralt  18977  m2detleiblem5  18994  m2detleiblem6  18995  m2detleiblem3  18998  m2detleiblem4  18999  m2detleib  19000  indistopon  19368  pptbas  19375  indistpsALT  19380  tuslem  20636  tmslem  20851  sqff1o  23321  dchrval  23374  eengv  24147  umgra1  24191  uslgra1  24237  usgra1  24238  usgraedgrnv  24242  usgrarnedg  24249  usgraedg4  24252  usgraexmpl  24266  usgraexmpledg  24268  cusgrarn  24324  wlkntrllem2  24427  wlkntrl  24429  constr1trl  24455  1pthon  24458  1pthon2v  24460  constr2trl  24466  constr2spth  24467  constr2pth  24468  2pthon  24469  2pthon3v  24471  usgra2adedgwlkon  24480  usg2wlk  24482  usg2wlkon  24483  constr3lem1  24510  constr3cyclpe  24528  3v3e3cycl2  24529  vdgr1b  24769  vdgr1a  24771  eupap1  24841  eupath2lem3  24844  eupath2  24845  vdegp1ai  24849  vdegp1bi  24850  frgraun  24861  frgra2v  24864  frgra3vlem1  24865  frgra3vlem2  24866  frgrancvvdeqlem3  24897  ex-uni  25012  ex-eprel  25019  indf1ofs  27905  prsiga  27997  difelsiga  27999  measssd  28052  eulerpartlemn  28186  probun  28224  coinflipprob  28284  coinflipspace  28285  coinfliprv  28287  coinflippv  28288  subfacp1lem3  28492  subfacp1lem5  28494  altopex  29578  altopthsn  29579  altxpsspw  29595  kelac2lem  30978  kelac2  30979  mendval  31101  prelpw  32133  mapprop  32643  zlmodzxzlmod  32651  zlmodzxzel  32652  zlmodzxz0  32653  zlmodzxzscm  32654  zlmodzxzadd  32655  zlmodzxzldeplem1  32811  zlmodzxzldeplem3  32813  zlmodzxzldeplem4  32814  ldepsnlinclem1  32816  ldepsnlinclem2  32817  ldepsnlinc  32819  bj-elopg  34305  tgrpset  36173  hlhilset  37366