Theorem velsn 4605

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-sn 4590

This theorem is referenced by:  rabsneq  4608  dfpr2  4610  ralsnsg  4634  rexsns  4635  ralsng  4639  disjsn  4675  snprc  4681  snssb  4746  snssgOLD  4748  raldifsnb  4760  difprsnss  4763  pwpw0  4777  eqsn  4793  eqsndOLD  4795  snsspw  4808  dfnfc2  4893  uni0b  4897  uni0c  4898  iunid  5024  iunsn  5030  sndisj  5099  rext  5408  moabex  5419  exss  5423  otiunsndisj  5480  dffr6  5594  fconstmpt  5700  opeliunxp  5705  opeliun2xp  5706  rnep  5890  restidsing  6024  xpdifid  6141  dmsnopg  6186  sniota  6502  dfmpt3  6652  nfunsn  6900  fnsnfv  6940  dffv2  6956  fsn  7107  fnasrn  7117  fnsnbg  7138  fnsnbOLD  7140  fmptsng  7142  fmptsnd  7143  fvclss  7215  eqfunresadj  7335  eusvobj2  7379  sucexeloniOLD  7786  resf1extb  7910  opabex3d  7944  opabex3rd  7945  opabex3  7946  xpord2pred  8124  xpord3pred  8131  frrlem12  8276  frrlem13  8277  oarec  8526  mapdm0  8815  ixp0x  8899  snmapen  9009  xpsnen  9025  marypha2lem2  9387  elirrv  9549  cantnfp1lem1  9631  cantnfp1lem3  9633  djuunxp  9874  dfac5lem1  10076  dfac5lem2  10077  dfac5lem4  10079  dfac5lem4OLD  10081  fin1a2lem11  10363  axdc4lem  10408  axcclem  10410  ttukeylem7  10468  xrsupexmnf  13265  xrinfmexpnf  13266  iccid  13351  fzsn  13527  fzpr  13540  seqz  14015  hashf1  14422  pr2pwpr  14444  s3iunsndisj  14934  fsum2dlem  15736  incexc2  15804  prodsn  15928  prodsnf  15930  fprod2dlem  15946  ef0lem  16044  lcmfunsnlem2  16610  1nprm  16649  vdwapun  16945  prmodvdslcmf  17018  cshwsiun  17070  mgmidsssn0  18599  mnd1id  18707  0subm  18744  efmnd1bas  18820  smndex1basss  18832  smndex1mgm  18834  trivsubgsnd  19086  kerf1ghm  19179  ghmqusnsglem1  19212  ghmquskerlem1  19215  ghmqusker  19219  symg1bas  19321  pmtrprfvalrn  19418  gex1  19521  sylow2alem1  19547  lsmdisj2  19612  0frgp  19709  0cyg  19823  prmcyg  19824  dprddisj2  19971  ablfacrp  19998  lspdisj  21035  lidlnz  21152  mulgrhm2  21388  pzriprnglem10  21400  ocvin  21583  psrlidm  21871  mplcoe1  21944  mplcoe5  21947  psdmul  22053  maducoeval2  22527  madugsum  22530  en2top  22872  restsn  23057  ist1-3  23236  ordtt1  23266  cmpcld  23289  unisngl  23414  dissnlocfin  23416  ptopn2  23471  snfil  23751  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  haustsms2  24024  tsmsxplem1  24040  tsmsxplem2  24041  ust0  24107  dscopn  24461  nmoid  24630  limcdif  25777  ellimc2  25778  limcmpt  25784  limcres  25787  ply1remlem  26070  plyeq0lem  26115  plyremlem  26212  aaliou2  26248  radcnv0  26325  abelthlem2  26342  wilthlem2  26979  vmappw  27026  ppinprm  27062  chtnprm  27064  musumsum  27102  dchrhash  27182  lgsquadlem1  27291  lgsquadlem2  27292  ssltsn  27704  ssltleft  27782  ssltright  27783  cofcutr  27832  addsuniflem  27908  negsid  27947  negsunif  27961  ssltmul1  28050  ssltmul2  28051  precsexlem11  28119  onscutlt  28165  n0sfincut  28246  0reno  28348  cplgr1v  29357  rusgrnumwwlkb0  29901  frgrncvvdeq  30238  fusgr2wsp2nb  30263  hsn0elch  31177  cycpmrn  33100  qsxpid  33333  prmidl0  33421  ccfldextdgrr  33667  xrge0iifiso  33925  qqhval2  33972  esumnul  34038  esumrnmpt2  34058  esumfzf  34059  sibfof  34331  sitgaddlemb  34339  plymulx0  34538  signstf0  34559  prodfzo03  34594  circlemeth  34631  sconnpi1  35226  dffr5  35741  elima4  35763  brsingle  35905  dfiota3  35911  funpartfun  35931  dfrdg4  35939  fwddifn0  36152  bj-csbsnlem  36891  bj-axsn  37020  bj-axadj  37029  bj-pw0ALT  37037  bj-restsn  37070  bj-rest10  37076  mptsnunlem  37326  fvineqsneu  37399  matunitlindflem1  37610  poimirlem23  37637  poimirlem26  37640  poimirlem27  37641  grposnOLD  37876  0idl  38019  smprngopr  38046  isdmn3  38068  ressn2  38433  lshpdisj  38980  lsat0cv  39026  snatpsubN  39744  dibelval3  41141  dib1dim  41159  dvh2dim  41439  mapd0  41659  hdmap14lem13  41874  dvrelogpow2b  42056  sticksstones11  42144  unitscyglem4  42186  sn-iotalem  42209  prjspeclsp  42600  pellexlem5  42821  jm2.23  42985  flcidc  43159  tfsconcatrn  43331  snhesn  43775  snssiALTVD  44816  snssiALT  44817  permaxinf2lem  45002  fsneq  45200  iccintsng  45521  icoiccdif  45522  limcrecl  45627  lptioo2  45629  lptioo1  45630  limcresiooub  45640  limcresioolb  45641  cnrefiisplem  45827  icccncfext  45885  dvmptfprodlem  45942  dvnprodlem3  45946  dirkercncflem2  46102  fourierdlem40  46145  fourierdlem48  46152  fourierdlem51  46155  fourierdlem62  46166  fourierdlem66  46170  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem79  46183  fourierdlem93  46197  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fouriersw  46229  elaa2  46232  etransclem44  46276  rrxsnicc  46298  sge00  46374  absnsb  47028  funressnfv  47044  fsetsniunop  47050  dfdfat2  47129  tz6.12-afv  47174  tz6.12-afv2  47241  otiunsndisjX  47280  iccpartgtl  47427  iccpartgt  47428  iccpartleu  47429  iccpartgel  47430  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbnd  47810  dfclnbgr6  47856  dfnbgr6  47857  stgredgiun  47957  xpsnopab  48145  mo0sn  48804  tposres0  48865  setcsnterm  49479  2arwcatlem1  49584  2arwcat  49589  setc1onsubc  49591  aacllem  49790