Theorem prex 4909

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 4302), 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 4269	. . . . . 6 |- ( y = B -> { x , y } = { x , B } )
2	1	eleq1d 2686	. . . . 5 |- ( y = B -> ( { x , y } e. _V <-> { x , B } e. _V ) )
3		zfpair2 4907	. . . . 5 |- { x , y } e. _V
4	2, 3	vtoclg 3266	. . . 4 |- ( B e. _V -> { x , B } e. _V )
5		preq1 4268	. . . . 5 |- ( x = A -> { x , B } = { A , B } )
6	5	eleq1d 2686	. . . 4 |- ( x = A -> ( { x , B } e. _V <-> { A , B } e. _V ) )
7	4, 6	syl5ib 234	. . 3 |- ( x = A -> ( B e. _V -> { A , B } e. _V ) )
8	7	vtocleg 3279	. 2 |- ( A e. _V -> ( B e. _V -> { A , B } e. _V ) )
9		prprc1 4300	. . 3 |- ( -. A e. _V -> { A , B } = { B } )
10		snex 4908	. . 3 |- { B } e. _V
11	9, 10	syl6eqel 2709	. 2 |- ( -. A e. _V -> { A , B } e. _V )
12		prprc2 4301	. . 3 |- ( -. B e. _V -> { A , B } = { A } )
13		snex 4908	. . 3 |- { A } e. _V
14	12, 13	syl6eqel 2709	. 2 |- ( -. B e. _V -> { A , B } e. _V )
15	8, 11, 14	pm2.61nii 178	1 |- { A , B } e. _V

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   e. wcel 1990   _Vcvv 3200   {csn 4177   {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-nul 3916  df-sn 4178  df-pr 4180

This theorem is referenced by:  prelpw  4914  opex  4932  elopg  4934  opi2  4938  op1stb  4940  opth  4945  opeqsn  4967  opeqpr  4968  propssopi  4971  opthwiener  4976  uniop  4977  fr2nr  5092  xpsspw  5233  relop  5272  f1prex  6539  unex  6956  tpex  6957  pw2f1olem  8064  1sdom  8163  opthreg  8515  pr2ne  8828  dfac2  8953  intwun  9557  wunex2  9560  wuncval2  9569  intgru  9636  xrex  11829  pr2pwpr  13261  wwlktovfo  13701  prmreclem2  15621  prdsval  16115  isposix  16957  clatl  17116  ipoval  17154  mgm0b  17256  frmdval  17388  mgmnsgrpex  17418  sgrpnmndex  17419  symg2bas  17818  pmtrprfval  17907  pmtrprfvalrn  17908  psgnprfval1  17942  psgnprfval2  17943  isnzr2hash  19264  psgnghm  19926  psgnco  19929  evpmodpmf1o  19942  mdetralt  20414  m2detleiblem5  20431  m2detleiblem6  20432  m2detleiblem3  20435  m2detleiblem4  20436  m2detleib  20437  indistopon  20805  pptbas  20812  indistpsALT  20817  tuslem  22071  tmslem  22287  sqff1o  24908  dchrval  24959  eengv  25859  structvtxvallem  25909  structiedg0val  25911  upgrbi  25988  umgrbi  25996  upgr1e  26008  umgredg  26033  uspgr1e  26136  usgr1e  26137  uspgr1ewop  26140  uspgr2v1e2w  26143  usgr2v1e2w  26144  usgrexmplef  26151  usgrexmpledg  26154  1loopgrnb0  26398  1egrvtxdg1  26405  1egrvtxdg0  26407  umgr2v2evtx  26417  umgr2v2eiedg  26419  umgr2v2e  26421  umgr2v2enb1  26422  umgr2v2evd2  26423  vdegp1ai  26432  vdegp1bi  26433  wlk2v2elem2  27016  wlk2v2e  27017  eupth2lems  27098  frcond2  27131  frcond3  27133  nfrgr2v  27136  frgr3vlem1  27137  frgr3vlem2  27138  frgrncvvdeqlem2  27164  ex-uni  27283  ex-eprel  27290  indf1ofs  30088  prsiga  30194  difelsiga  30196  inelpisys  30217  measssd  30278  carsgsigalem  30377  carsgclctun  30383  pmeasmono  30386  eulerpartlemn  30443  probun  30481  coinflipprob  30541  coinflipspace  30542  coinfliprv  30544  coinflippv  30545  subfacp1lem3  31164  subfacp1lem5  31166  altopex  32067  altopthsn  32068  altxpsspw  32084  poimirlem9  33418  poimirlem15  33424  tgrpset  36033  hlhilset  37226  kelac2lem  37634  kelac2  37635  mendval  37753  fvrcllb0d  37985  fvrcllb0da  37986  fvrcllb1d  37987  corclrcl  37999  corcltrcl  38031  cotrclrcl  38034  clsk1indlem2  38340  clsk1indlem3  38341  clsk1indlem4  38342  clsk1indlem1  38343  prsal  40538  sge0pr  40611  nnsum3primes4  41676  nnsum3primesgbe  41680  elsprel  41725  sprvalpw  41730  mapprop  42124  zlmodzxzlmod  42132  zlmodzxzel  42133  zlmodzxz0  42134  zlmodzxzscm  42135  zlmodzxzadd  42136  zlmodzxzldeplem1  42289  zlmodzxzldeplem3  42291  zlmodzxzldeplem4  42292  ldepsnlinclem1  42294  ldepsnlinclem2  42295  ldepsnlinc  42297  onsetreclem1  42448