Theorem snex 4632

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4580. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.)

Assertion

Ref	Expression
snex	|- { A } e. _V

Proof of Theorem snex

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsn2 3985	. . 3 |- { A } = { A , A }
2		preq12 4053	. . . . . 6 |- ( ( x = A /\ x = A ) -> { x , x } = { A , A } )
3	2	anidms 643	. . . . 5 |- ( x = A -> { x , x } = { A , A } )
4	3	eleq1d 2471	. . . 4 |- ( x = A -> ( { x , x } e. _V <-> { A , A } e. _V ) )
5		zfpair2 4631	. . . 4 |- { x , x } e. _V
6	4, 5	vtoclg 3117	. . 3 |- ( A e. _V -> { A , A } e. _V )
7	1, 6	syl5eqel 2494	. 2 |- ( A e. _V -> { A } e. _V )
8		snprc 4035	. . . 4 |- ( -. A e. _V <-> { A } = (/) )
9	8	biimpi 194	. . 3 |- ( -. A e. _V -> { A } = (/) )
10		0ex 4526	. . 3 |- (/) e. _V
11	9, 10	syl6eqel 2498	. 2 |- ( -. A e. _V -> { A } e. _V )
12	7, 11	pm2.61i 164	1 |- { A } e. _V

Syntax hints:   -. wn 3   = wceq 1405   e. wcel 1842   _Vcvv 3059   (/)c0 3738   {csn 3972   {cpr 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pr 4630

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-v 3061  df-dif 3417  df-un 3419  df-nul 3739  df-sn 3973  df-pr 3975

This theorem is referenced by:  prex  4633  elALT  4634  dtruALT2  4635  snelpwi  4636  snelpw  4637  rext  4639  sspwb  4640  intid  4649  moabex  4650  nnullss  4653  exss  4654  opi1  4658  op1stb  4661  opnz  4662  opeqsn  4686  opeqpr  4687  opthwiener  4692  uniop  4693  frirr  4800  frsn  4894  xpsspw  4937  relop  4974  onnev  5530  funopg  5601  fsnex  6169  tpex  6581  snnex  6588  difsnexi  6590  sucexb  6627  soex  6727  elxp4  6728  elxp5  6729  opabex3d  6762  opabex3  6763  1stval  6786  2ndval  6787  fo1st  6804  fo2nd  6805  mpt2exxg  6858  cnvf1o  6883  fnse  6901  suppsnop  6916  brtpos2  6964  wfrlem15  7035  tfrlem12  7092  tfrlem16  7096  mapsn  7498  fvdiagfn  7501  mapsnconst  7502  mapsncnv  7503  mapsnf1o2  7504  ralxpmap  7506  elixpsn  7546  ixpsnf1o  7547  mapsnf1o  7548  ensn1  7617  en1b  7621  mapsnen  7631  xpsnen  7639  endisj  7642  xpsnen2g  7648  domunsncan  7655  enfixsn  7664  domunsn  7705  fodomr  7706  disjenex  7713  domssex2  7715  domssex  7716  map2xp  7725  phplem2  7735  isinf  7768  pssnn  7773  findcard2  7794  ac6sfi  7798  xpfi  7825  fodomfi  7833  pwfilem  7848  fczfsuppd  7881  snopfsupp  7886  fisn  7921  marypha1lem  7927  brwdom2  8033  unxpwdom2  8048  elirrv  8057  epfrs  8194  tc2  8205  tcsni  8206  ranksuc  8315  fseqenlem1  8437  dfac5lem2  8537  dfac5lem3  8538  dfac5lem4  8539  kmlem2  8563  cdafn  8581  cdaval  8582  cdaassen  8594  mapcdaen  8596  cdadom1  8598  cdainf  8604  ackbij1lem5  8636  cfsuc  8669  isfin1-3  8798  hsmexlem4  8841  axcc2lem  8848  dcomex  8859  axdc3lem4  8865  axdc4lem  8867  ttukeylem3  8923  brdom7disj  8941  brdom6disj  8942  fpwwe2lem13  9050  canthwe  9059  canthp1lem1  9060  uniwun  9148  rankcf  9185  nn0ex  10842  hashxplem  12540  hashmap  12542  hashbclem  12550  hashf1lem1  12553  hashge3el3dif  12573  climconst2  13520  incexclem  13799  ramub1lem2  14754  cshwsex  14794  setsvalg  14865  setsid  14884  pwsbas  15101  pwsle  15106  pwssca  15110  pwssnf1o  15112  imasplusg  15131  imasmulr  15132  imasvsca  15134  imasip  15135  xpsc  15171  acsfn  15273  isfunc  15477  homaf  15633  homaval  15634  funcsetcestrclem1  15747  mgm1  16208  sgrp1  16242  mnd1  16285  mnd1OLD  16286  mnd1id  16287  grp1  16466  symg2bas  16747  idrespermg  16760  pmtrsn  16868  psgnsn  16869  abl1  17196  gsum2d2  17323  gsumcom2  17324  dprdz  17397  dprdsn  17403  dprd2da  17411  ring1  17568  pwssplit3  18027  drngnidl  18197  drnglpir  18221  rng1nnzr  18242  evlssca  18511  mpfind  18525  evls1sca  18680  pf1ind  18711  frlmip  19105  islindf4  19165  mattposvs  19249  mat1dimelbas  19265  mat1dimscm  19269  mat1dimmul  19270  mat1rhmval  19273  m1detdiag  19391  mdetrlin  19396  mdetrsca2  19398  mdetrlin2  19401  mdetunilem5  19410  smadiadetglem2  19466  basdif0  19746  ordtbas  19986  leordtval2  20006  dishaus  20176  discmp  20191  concompid  20224  dis2ndc  20253  dislly  20290  dis1stc  20292  unisngl  20320  1stckgen  20347  ptbasfi  20374  dfac14lem  20410  dfac14  20411  ptrescn  20432  xkoptsub  20447  pt1hmeo  20599  xpstopnlem1  20602  ptcmpfi  20606  isufil2  20701  ufileu  20712  filufint  20713  uffix  20714  uffixsn  20718  flimclslem  20777  ptcmplem1  20844  cnextfval  20854  imasdsf1olem  21168  icccmplem1  21619  icccmplem2  21620  rrxip  22114  elply2  22885  plyss  22888  plyeq0lem  22899  taylfval  23046  axlowdimlem15  24676  axlowdim  24681  umgra1  24743  uslgra1  24789  usgra1  24790  usgra1v  24807  cusgra1v  24878  uvtx01vtx  24909  wlkntrl  24981  0pthonv  25000  constr1trl  25007  1pthon  25010  1pthon2v  25012  1conngra  25092  vdgr1d  25320  vdgr1b  25321  vdgr1a  25323  grposn  25631  zrdivrng  25848  0ofval  26116  resf1o  28000  ordtconlem1  28359  esumpr  28513  esumrnmpt2  28515  esumfzf  28516  esum2dlem  28539  esum2d  28540  esumiun  28541  prsiga  28579  rossros  28628  cntnevol  28676  carsgclctunlem1  28765  omsmeas  28771  eulerpartlemgs2  28825  ccatmulgnn0dir  29002  ofs1  29005  ofcs1  29006  bnj918  29151  bnj95  29249  bnj1452  29435  bnj1489  29439  subfacp1lem5  29481  erdszelem5  29492  erdszelem8  29495  cvmliftlem4  29585  cvmliftlem5  29586  cvmlift2lem6  29605  cvmlift2lem9  29608  cvmlift2lem12  29611  fobigcup  30238  elsingles  30256  fnsingle  30257  fvsingle  30258  dfiota3  30261  brapply  30276  brsuccf  30279  funpartlem  30280  altopthsn  30299  altxpsspw  30315  hfsn  30517  neibastop2lem  30588  topjoin  30593  onpsstopbas  30662  bj-sels  31085  bj-snsetex  31086  bj-elsngl  31091  bj-2uplex  31145  bj-elopg  31167  f1omptsnlem  31252  mptsnunlem  31254  topdifinffinlem  31264  finixpnum  31410  ptrest  31420  fdc  31520  heiborlem3  31591  heiborlem8  31596  ismrer1  31616  ldualset  32143  lineset  32755  ispointN  32759  dvaset  34024  dvhset  34101  dibval  34162  dibfna  34174  elrfi  34988  mzpincl  35028  mzpcompact2lem  35045  wopprc  35334  dfac11  35370  kelac2  35373  pwslnmlem1  35400  pwslnm  35402  fvilbdRP  35669  brtrclfv2  35706  frege110  35954  frege133  35977  snelpwrVD  36661  fnchoice  36784  limcresiooub  37016  limcresioolb  37017  cnfdmsn  37052  dvsinax  37076  fourierdlem48  37305  fourierdlem49  37306  nnsum3primesprm  37838  mpt2exxg2  38438  mapsnop  38445  lindsrng01  38580  snlindsntorlem  38582  snlindsntor  38583  lmod1lem1  38599  lmod1lem2  38600  lmod1lem3  38601  lmod1lem4  38602  lmod1lem5  38603  lmod1  38604  lmod1zr  38605  aacllem  38860