Theorem prex 4539

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 3992), 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 3960	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2509	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4537	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 3035	. . . 4 |- ( B e. _V -> { x , B } e. _V )
5		preq1 3959	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2509	. . . 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 3048	. 2 |- ( A e. _V -> ( B e. _V -> { A , B } e. _V ) )
9		prprc1 3990	. . 3 |- ( -. A e. _V -> { A , B } = { B } )
10		snex 4538	. . 3 |- { B } e. _V
11	9, 10	syl6eqel 2531	. 2 |- ( -. A e. _V -> { A , B } e. _V )
12		prprc2 3991	. . 3 |- ( -. B e. _V -> { A , B } = { A } )
13		snex 4538	. . 3 |- { A } e. _V
14	12, 13	syl6eqel 2531	. 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 1369   e. wcel 1756   _Vcvv 2977   {csn 3882   {cpr 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-v 2979  df-dif 3336  df-un 3338  df-nul 3643  df-sn 3883  df-pr 3885

This theorem is referenced by:  prelpwi  4544  opex  4561  opi2  4565  op1stb  4567  opth  4571  opeqsn  4592  opeqpr  4593  opthwiener  4598  uniop  4599  fr2nr  4703  xpsspwOLD  4959  relop  4995  unex  6383  tpex  6384  pw2f1olem  7420  1sdom  7520  opthreg  7829  pr2ne  8177  dfac2  8305  intwun  8907  wunex2  8910  wuncval2  8919  intgru  8986  xrex  10993  pr2pwpr  12188  prmreclem2  13983  prdsval  14398  isposix  15132  clatl  15291  ipoval  15329  frmdval  15534  symg2bas  15908  pmtrprfval  15998  pmtrprfvalrn  15999  psgnprfval1  16031  psgnprfval2  16032  psgnghm  18015  psgnco  18018  evpmodpmf1o  18031  mdetralt  18419  m2detleiblem5  18436  m2detleiblem6  18437  m2detleiblem3  18440  m2detleiblem4  18441  m2detleib  18442  indistopon  18610  pptbas  18617  indistpsALT  18622  tuslem  19847  tmslem  20062  sqff1o  22525  dchrval  22578  eengv  23230  umgra1  23265  uslgra1  23296  usgra1  23297  usgraedgrnv  23301  usgrarnedg  23308  usgraedg4  23310  usgraexmpl  23324  cusgrarn  23372  wlkntrllem2  23464  wlkntrl  23466  constr1trl  23492  1pthon  23495  1pthon2v  23497  constr2wlk  23502  constr2trl  23503  constr2spth  23504  constr2pth  23505  2pthon  23506  2pthon3v  23508  constr3lem1  23536  constr3cyclpe  23554  3v3e3cycl2  23555  vdgr1b  23579  vdgr1a  23581  eupap1  23602  eupath2lem3  23605  eupath2  23606  vdegp1ai  23610  vdegp1bi  23611  ex-uni  23638  ex-eprel  23645  indf1ofs  26487  prsiga  26579  difelsiga  26581  measssd  26634  eulerpartlemn  26769  probun  26807  coinflipprob  26867  coinflipspace  26868  coinfliprv  26870  subfacp1lem3  27075  subfacp1lem5  27077  altopex  27996  altopthsn  27997  altxpsspw  28013  kelac2lem  29422  kelac2  29423  mendval  29545  wwlktovfo  30258  usgra2adedgwlkon  30312  usg2wlk  30314  usg2wlkon  30315  frgraun  30593  frgra2v  30596  frgra3vlem1  30597  frgra3vlem2  30598  frgrancvvdeqlem3  30630  mapprop  30741  zlmodzxzlmod  30756  zlmodzxzel  30757  zlmodzxz0  30758  zlmodzxzscm  30759  zlmodzxzadd  30760  isnzr2hash  30779  zlmodzxzldeplem1  31047  zlmodzxzldeplem3  31049  zlmodzxzldeplem4  31050  ldepsnlinclem1  31052  ldepsnlinclem2  31053  ldepsnlinc  31055  bj-elopg  32527  tgrpset  34394  hlhilset  35587