Theorem velsn 4583

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 3497	. 2 ⊢ 𝑥 ∈ V
2	1	elsn 4582	1 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-sn 4568

This theorem is referenced by:  dfpr2  4586  ralsnsg  4608  rexsns  4609  disjsn  4647  snprc  4653  snssg  4717  raldifsnb  4729  difprsnss  4732  pwpw0  4746  eqsn  4762  snsspw  4775  pwsnOLD  4831  dfnfc2  4860  uni0b  4864  uni0c  4865  sndisj  5057  rext  5341  moabex  5351  exss  5355  otiunsndisj  5410  fconstmpt  5614  opeliunxp  5619  rnep  5797  restidsing  5922  xpdifid  6025  dmsnopg  6070  sniota  6346  dfmpt3  6482  nfunsn  6707  dffv2  6756  fsn  6897  fnasrn  6907  fnsnb  6928  fmptsng  6930  fmptsnd  6931  fvclss  7001  eusvobj2  7149  suceloni  7528  opabex3d  7666  opabex3rd  7667  opabex3  7668  wfrlem14  7968  wfrlem15  7969  oarec  8188  mapdm0  8421  ixp0x  8490  snmapen  8590  xpsnen  8601  marypha2lem2  8900  elirrv  9060  cantnfp1lem1  9141  cantnfp1lem3  9143  djuunxp  9350  dfac5lem1  9549  dfac5lem2  9550  dfac5lem4  9552  fin1a2lem11  9832  axdc4lem  9877  axcclem  9879  ttukeylem7  9937  xrsupexmnf  12699  xrinfmexpnf  12700  iccid  12784  fzsn  12950  fzpr  12963  seqz  13419  hashf1  13816  pr2pwpr  13838  s3iunsndisj  14328  fsum2dlem  15125  incexc2  15193  prodsn  15316  prodsnf  15318  fprod2dlem  15334  ef0lem  15432  lcmfunsnlem2  15984  1nprm  16023  vdwapun  16310  prmodvdslcmf  16383  cshwsiun  16433  mgmidsssn0  17882  mnd1id  17953  0subm  17982  efmnd1bas  18058  smndex1basss  18070  smndex1mgm  18072  trivsubgsnd  18306  symg1bas  18519  pmtrprfvalrn  18616  gex1  18716  sylow2alem1  18742  lsmdisj2  18808  0frgp  18905  0cyg  19013  prmcyg  19014  dprddisj2  19161  ablfacrp  19188  kerf1ghm  19497  kerf1hrmOLD  19498  lspdisj  19897  lidlnz  20001  psrlidm  20183  mplcoe1  20246  mplcoe5  20249  mulgrhm2  20646  ocvin  20818  maducoeval2  21249  madugsum  21252  en2top  21593  restsn  21778  ist1-3  21957  ordtt1  21987  cmpcld  22010  unisngl  22135  dissnlocfin  22137  ptopn2  22192  snfil  22472  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  haustsms2  22745  tsmsxplem1  22761  tsmsxplem2  22762  ust0  22828  dscopn  23183  nmoid  23351  limcdif  24474  ellimc2  24475  limcmpt  24481  limcres  24484  ply1remlem  24756  plyeq0lem  24800  plyremlem  24893  aaliou2  24929  radcnv0  25004  abelthlem2  25020  wilthlem2  25646  vmappw  25693  ppinprm  25729  chtnprm  25731  musumsum  25769  dchrhash  25847  lgsquadlem1  25956  lgsquadlem2  25957  cplgr1v  27212  rusgrnumwwlkb0  27750  frgrncvvdeq  28088  fusgr2wsp2nb  28113  hsn0elch  29025  eqsnd  30289  cycpmrn  30785  qsxpid  30927  ccfldextdgrr  31057  xrge0iifiso  31178  qqhval2  31223  esumnul  31307  esumrnmpt2  31327  esumfzf  31328  sibfof  31598  sitgaddlemb  31606  plymulx0  31817  signstf0  31838  prodfzo03  31874  circlemeth  31911  bnj521  32007  sconnpi1  32486  dffr5  32989  eqfunresadj  33004  elima4  33019  frrlem12  33134  frrlem13  33135  brsingle  33378  dfiota3  33384  funpartfun  33404  dfrdg4  33412  fwddifn0  33625  bj-csbsnlem  34223  bj-pw0ALT  34345  bj-restsn  34376  bj-rest10  34382  mptsnunlem  34622  fvineqsneu  34695  matunitlindflem1  34903  poimirlem23  34930  poimirlem26  34933  poimirlem27  34934  grposnOLD  35175  0idl  35318  smprngopr  35345  isdmn3  35367  lshpdisj  36138  lsat0cv  36184  snatpsubN  36901  dibelval3  38298  dib1dim  38316  dvh2dim  38596  mapd0  38816  hdmap14lem13  39031  iunsn  39138  fnsnbt  39140  prjspeclsp  39282  pellexlem5  39450  jm2.23  39613  flcidc  39794  snhesn  40152  snssiALTVD  41181  snssiALT  41182  fsneq  41489  iccintsng  41819  icoiccdif  41820  limcrecl  41930  lptioo2  41932  lptioo1  41933  limcresiooub  41943  limcresioolb  41944  cnrefiisplem  42130  icccncfext  42190  dvmptfprodlem  42249  dvnprodlem3  42253  dirkercncflem2  42409  fourierdlem40  42452  fourierdlem48  42459  fourierdlem51  42462  fourierdlem62  42473  fourierdlem66  42477  fourierdlem74  42485  fourierdlem75  42486  fourierdlem76  42487  fourierdlem78  42489  fourierdlem79  42490  fourierdlem93  42504  fourierdlem101  42512  fourierdlem103  42514  fourierdlem104  42515  fouriersw  42536  elaa2  42539  etransclem44  42583  rrxsnicc  42605  sge00  42678  absnsb  43282  funressnfv  43298  dfdfat2  43347  tz6.12-afv  43392  tz6.12-afv2  43459  otiunsndisjX  43498  iccpartgtl  43606  iccpartgt  43607  iccpartleu  43608  iccpartgel  43609  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  bgoldbtbnd  43994  xpsnopab  44052  opeliun2xp  44401  aacllem  44922