Theorem velsn 4141

Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
velsn	⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)

Proof of Theorem velsn

Step	Hyp	Ref	Expression
1		vex 3176	. 2 ⊢ 𝑥 ∈ V
2	1	elsn 4140	1 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)

Syntax hints:   ↔ wb 195   = wceq 1475   ∈ wcel 1977  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-sn 4126

This theorem is referenced by:  dfpr2  4143  ralsnsg  4163  rexsns  4164  disjsn  4192  snprc  4197  euabsn2  4204  snss  4259  raldifsnb  4266  difprsnss  4270  pwpw0  4284  eqsn  4301  eqsnOLD  4302  snsspw  4315  pwsnALT  4367  dfnfc2  4390  dfnfc2OLD  4391  uni0b  4399  uni0c  4400  sndisj  4574  rext  4843  moabex  4854  exss  4858  otiunsndisj  4905  fconstmpt  5085  opeliunxp  5093  restidsing  5377  restidsingOLD  5378  xpdifid  5481  dmsnopg  5524  elsnxpOLD  5595  sniota  5795  dfmpt3  5927  nfunsn  6135  dffv2  6181  fsn  6308  fnasrn  6317  fnsnb  6337  fmptsng  6339  fmptsnd  6340  fvclss  6404  eusvobj2  6542  suceloni  6905  opabex3d  7037  opabex3  7038  wfrlem14  7315  wfrlem15  7316  oarec  7529  ixp0x  7822  xpsnen  7929  marypha2lem2  8225  elirrv  8387  cantnfp1lem1  8458  cantnfp1lem3  8460  dfac5lem1  8829  dfac5lem2  8830  dfac5lem4  8832  fin1a2lem11  9115  axdc4lem  9160  axcclem  9162  ttukeylem7  9220  xrsupexmnf  12007  xrinfmexpnf  12008  iccid  12091  fzsn  12254  fzpr  12266  seqz  12711  hashf1  13098  pr2pwpr  13116  fundmge2nop0  13129  s3iunsndisj  13555  fsum2dlem  14343  incexc2  14409  prodsn  14531  prodsnf  14533  fprod2dlem  14549  ef0lem  14648  divalgmodOLD  14968  lcmfunsnlem2  15191  1nprm  15230  isprm2lem  15232  vdwapun  15516  prmodvdslcmf  15589  cshwsiun  15644  xpsc0  16043  xpsc1  16044  mgmidsssn0  17092  mnd1id  17155  symg1bas  17639  pmtrprfvalrn  17731  gex1  17829  sylow2alem1  17855  lsmdisj2  17918  0frgp  18015  0cyg  18117  prmcyg  18118  dprddisj2  18261  ablfacrp  18288  kerf1hrm  18566  lspdisj  18946  lidlnz  19049  psrlidm  19224  mplcoe1  19286  mplcoe5  19289  evlslem1  19336  mulgrhm2  19666  ocvin  19837  maducoeval2  20265  madugsum  20268  en2top  20600  restsn  20784  ist1-3  20963  ordtt1  20993  cmpcld  21015  unisngl  21140  dissnlocfin  21142  ptopn2  21197  snfil  21478  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  haustsms2  21750  tsmsxplem1  21766  tsmsxplem2  21767  ust0  21833  dscopn  22188  nmoid  22356  limcdif  23446  ellimc2  23447  limcmpt  23453  limcres  23456  ply1remlem  23726  plyeq0lem  23770  plyremlem  23863  aaliou2  23899  radcnv0  23974  abelthlem2  23990  wilthlem2  24595  vmappw  24642  ppinprm  24678  chtnprm  24680  musumsum  24718  dchrhash  24796  lgsquadlem1  24905  lgsquadlem2  24906  isusgra0  25876  usgraop  25879  nbcusgra  25992  usgrasscusgra  26011  rusgranumwlkb0  26480  frgrancvvdeqlem9  26568  frgrawopreglem4  26574  usg2spot2nb  26592  hsn0elch  27489  iunxsngf  28758  xrge0iifiso  29309  qqhval2  29354  esumnul  29437  esumrnmpt2  29457  esumfzf  29458  sibfof  29729  sitgaddlemb  29737  plymulx0  29950  signstf0  29971  signstfvneq0  29975  bnj145OLD  30049  bnj521  30059  sconpi1  30475  dffr5  30896  elima4  30924  brsingle  31194  dfiota3  31200  funpartfun  31220  dfrdg4  31228  fwddifn0  31441  bj-csbsnlem  32090  bj-restsn  32216  bj-rest10  32222  mptsnunlem  32361  matunitlindflem1  32575  poimirlem23  32602  poimirlem26  32605  poimirlem27  32606  grposnOLD  32851  0idl  32994  smprngopr  33021  isdmn3  33043  lshpdisj  33292  lsat0cv  33338  snatpsubN  34054  dibelval3  35454  dib1dim  35472  dvh2dim  35752  mapd0  35972  hdmap14lem13  36190  pellexlem5  36415  jm2.23  36581  flcidc  36763  snhesn  37100  snssiALTVD  38084  snssiALT  38085  fsneq  38393  iccintsng  38596  icoiccdif  38597  limcrecl  38696  lptioo2  38698  lptioo1  38699  limcresiooub  38709  limcresioolb  38710  icccncfext  38773  dvmptfprodlem  38834  dvnprodlem3  38838  dirkercncflem2  38997  fourierdlem40  39040  fourierdlem48  39047  fourierdlem51  39050  fourierdlem62  39061  fourierdlem66  39065  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem79  39078  fourierdlem93  39092  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fouriersw  39124  elaa2  39127  etransclem44  39171  rrxsnicc  39196  sge00  39269  funressnfv  39857  dfdfat2  39860  tz6.12-afv  39902  iccpartgtl  39964  iccpartgt  39965  iccpartleu  39966  iccpartgel  39967  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbnd  40225  otiunsndisjX  40317  cplgr1v  40652  rusgrnumwwlkb0  41174  frgrncvvdeq  41480  frgrwopreglem4  41484  fusgr2wsp2nb  41498  xpsnopab  41555  opeliun2xp  41904  aacllem  42356