Theorem snex 4365

Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4345. (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 3788	. . 3 |- { A } = { A , A }
2		preq12 3845	. . . . . 6 |- ( ( x = A /\ x = A ) -> { x , x } = { A , A } )
3	2	anidms 627	. . . . 5 |- ( x = A -> { x , x } = { A , A } )
4	3	eleq1d 2470	. . . 4 |- ( x = A -> ( { x , x } e. _V <-> { A , A } e. _V ) )
5		zfpair2 4364	. . . 4 |- { x , x } e. _V
6	4, 5	vtoclg 2971	. . 3 |- ( A e. _V -> { A , A } e. _V )
7	1, 6	syl5eqel 2488	. 2 |- ( A e. _V -> { A } e. _V )
8		snprc 3831	. . . 4 |- ( -. A e. _V <-> { A } = (/) )
9	8	biimpi 187	. . 3 |- ( -. A e. _V -> { A } = (/) )
10		0ex 4299	. . 3 |- (/) e. _V
11	9, 10	syl6eqel 2492	. 2 |- ( -. A e. _V -> { A } e. _V )
12	7, 11	pm2.61i 158	1 |- { A } e. _V

Syntax hints:   -. wn 3   = wceq 1649   e. wcel 1721   _Vcvv 2916   (/)c0 3588   {csn 3774   {cpr 3775

This theorem is referenced by:  prex  4366  elALT  4367  dtruALT2  4368  snelpwi  4369  snelpw  4370  rext  4372  sspwb  4373  intid  4381  moabex  4382  nnullss  4385  exss  4386  opi1  4390  opnz  4392  opeqsn  4412  opeqpr  4413  opthwiener  4418  uniop  4419  frirr  4519  tpex  4667  snnex  4672  op1stb  4717  sucexb  4748  frsn  4907  onnev  4917  xpsspwOLD  4946  relop  4982  soex  5278  elxp4  5316  elxp5  5317  funopg  5444  opabex3d  5948  opabex3  5949  1stval  6310  2ndval  6311  fo1st  6325  fo2nd  6326  mpt2exxg  6381  cnvf1o  6404  fnse  6422  brtpos2  6444  tfrlem12  6609  tfrlem16  6613  mapsn  7014  fvdiagfn  7017  mapsnconst  7018  mapsncnv  7019  mapsnf1o2  7020  elixpsn  7060  ixpsnf1o  7061  mapsnf1o  7062  ensn1  7130  en1b  7134  mapsnen  7143  xpsnen  7151  endisj  7154  xpsnen2g  7160  domunsncan  7167  domunsn  7216  fodomr  7217  disjenex  7224  domssex2  7226  domssex  7227  map2xp  7236  phplem2  7246  isinf  7281  pssnn  7286  findcard2  7307  ac6sfi  7310  xpfi  7337  fodomfi  7344  pwfilem  7359  fisn  7390  marypha1lem  7396  brwdom2  7497  unxpwdom2  7512  elirrv  7521  epfrs  7623  tc2  7637  tcsni  7638  ranksuc  7747  fseqenlem1  7861  dfac5lem2  7961  dfac5lem3  7962  dfac5lem4  7963  kmlem2  7987  cdafn  8005  cdaval  8006  cdaassen  8018  mapcdaen  8020  cdadom1  8022  cdainf  8028  ackbij1lem5  8060  cfsuc  8093  isfin1-3  8222  hsmexlem4  8265  axcc2lem  8272  dcomex  8283  axdc3lem4  8289  axdc4lem  8291  ttukeylem3  8347  brdom7disj  8365  brdom6disj  8366  fpwwe2lem13  8473  canthwe  8482  canthp1lem1  8483  uniwun  8571  rankcf  8608  nn0ex  10183  hashxplem  11651  hashmap  11653  hashbclem  11656  hashf1lem1  11659  climconst2  12297  incexclem  12571  ramub1lem2  13350  setsvalg  13447  setsid  13463  pwsbas  13664  pwsle  13669  pwssca  13673  pwssnf1o  13675  imasplusg  13698  imasmulr  13699  imasvsca  13701  xpsc  13737  acsfn  13839  isfunc  14016  homaf  14140  homaval  14141  gsum2d2  15503  gsumcom2  15504  dprdz  15543  dprdsn  15549  dprd2da  15555  drngnidl  16255  drnglpir  16279  basdif0  16973  ordtbas  17210  leordtval2  17230  dishaus  17400  discmp  17415  concompid  17447  dis2ndc  17476  dislly  17513  dis1stc  17515  1stckgen  17539  ptbasfi  17566  dfac14lem  17602  dfac14  17603  ptrescn  17624  xkoptsub  17639  pt1hmeo  17791  xpstopnlem1  17794  ptcmpfi  17798  isufil2  17893  ufileu  17904  filufint  17905  uffix  17906  uffixsn  17910  flimclslem  17969  ptcmplem1  18036  cnextfval  18046  imasdsf1olem  18356  icccmplem1  18806  icccmplem2  18807  evlssca  19896  mpfind  19918  pf1ind  19928  elply2  20068  plyss  20071  plyeq0lem  20082  taylfval  20228  umgra1  21314  uslgra1  21345  usgra1  21346  usgra1v  21362  cusgra1v  21423  uvtx01vtx  21454  wlkntrl  21515  0pthonv  21534  constr1trl  21541  1pthon  21544  1pthon2v  21546  1conngra  21615  vdgr1d  21627  vdgr1b  21628  vdgr1a  21630  grposn  21756  zrdivrng  21973  0ofval  22241  esumpr  24410  esumfzf  24412  prsiga  24467  cntnevol  24535  subfacp1lem5  24823  erdszelem5  24834  erdszelem8  24837  cvmliftlem4  24928  cvmliftlem5  24929  cvmlift2lem6  24948  cvmlift2lem9  24951  cvmlift2lem12  24954  wfrlem15  25484  fobigcup  25654  elsingles  25671  fnsingle  25672  fvsingle  25673  dfiota3  25676  brapply  25691  brsuccf  25694  funpartlem  25695  altopthsn  25710  altxpsspw  25726  axlowdimlem15  25799  axlowdim  25804  hfsn  26024  onpsstopbas  26084  neibastop2lem  26279  topjoin  26284  fdc  26339  heiborlem3  26412  heiborlem8  26417  ismrer1  26437  ralxpmap  26632  elrfi  26638  mzpincl  26681  mzpcompact2lem  26698  wopprc  26991  dfac11  27028  kelac2  27031  pwssplit3  27058  pwslnmlem1  27062  pwslnm  27064  enfixsn  27125  islindf4  27176  fnchoice  27567  snelpwrVD  28652  bnj918  28841  bnj95  28941  bnj1452  29127  bnj1489  29131  ldualset  29608  lineset  30220  ispointN  30224  dvaset  31487  dvhset  31564  dibval  31625  dibfna  31637

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-un 3285  df-nul 3589  df-sn 3780  df-pr 3781