Theorem velsn 4574

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2108  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-sn 4559

This theorem is referenced by:  dfpr2  4577  ralsnsg  4601  rexsns  4602  ralsng  4606  disjsn  4644  snprc  4650  snssg  4715  raldifsnb  4726  difprsnss  4729  pwpw0  4743  eqsn  4759  snsspw  4772  pwsnOLD  4829  dfnfc2  4860  uni0b  4864  uni0c  4865  iunsn  4991  sndisj  5061  rext  5358  moabex  5368  exss  5372  otiunsndisj  5428  dffr6  5538  fconstmpt  5640  opeliunxp  5645  rnep  5825  restidsing  5951  xpdifid  6060  dmsnopg  6105  sniota  6409  dfmpt3  6551  nfunsn  6793  fnsnfv  6829  dffv2  6845  fsn  6989  fnasrn  6999  fnsnb  7020  fmptsng  7022  fmptsnd  7023  fvclss  7097  eusvobj2  7248  suceloni  7635  opabex3d  7781  opabex3rd  7782  opabex3  7783  frrlem12  8084  frrlem13  8085  wfrlem14OLD  8124  wfrlem15OLD  8125  oarec  8355  mapdm0  8588  ixp0x  8672  snmapen  8782  xpsnen  8796  marypha2lem2  9125  elirrv  9285  cantnfp1lem1  9366  cantnfp1lem3  9368  djuunxp  9610  dfac5lem1  9810  dfac5lem2  9811  dfac5lem4  9813  fin1a2lem11  10097  axdc4lem  10142  axcclem  10144  ttukeylem7  10202  xrsupexmnf  12968  xrinfmexpnf  12969  iccid  13053  fzsn  13227  fzpr  13240  seqz  13699  hashf1  14099  pr2pwpr  14121  s3iunsndisj  14607  fsum2dlem  15410  incexc2  15478  prodsn  15600  prodsnf  15602  fprod2dlem  15618  ef0lem  15716  lcmfunsnlem2  16273  1nprm  16312  vdwapun  16603  prmodvdslcmf  16676  cshwsiun  16729  mgmidsssn0  18271  mnd1id  18342  0subm  18371  efmnd1bas  18447  smndex1basss  18459  smndex1mgm  18461  trivsubgsnd  18697  symg1bas  18913  pmtrprfvalrn  19011  gex1  19111  sylow2alem1  19137  lsmdisj2  19203  0frgp  19300  0cyg  19409  prmcyg  19410  dprddisj2  19557  ablfacrp  19584  kerf1ghm  19902  lspdisj  20302  lidlnz  20412  mulgrhm2  20612  ocvin  20791  psrlidm  21082  mplcoe1  21148  mplcoe5  21151  maducoeval2  21697  madugsum  21700  en2top  22043  restsn  22229  ist1-3  22408  ordtt1  22438  cmpcld  22461  unisngl  22586  dissnlocfin  22588  ptopn2  22643  snfil  22923  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  haustsms2  23196  tsmsxplem1  23212  tsmsxplem2  23213  ust0  23279  dscopn  23635  nmoid  23812  limcdif  24945  ellimc2  24946  limcmpt  24952  limcres  24955  ply1remlem  25232  plyeq0lem  25276  plyremlem  25369  aaliou2  25405  radcnv0  25480  abelthlem2  25496  wilthlem2  26123  vmappw  26170  ppinprm  26206  chtnprm  26208  musumsum  26246  dchrhash  26324  lgsquadlem1  26433  lgsquadlem2  26434  cplgr1v  27700  rusgrnumwwlkb0  28237  frgrncvvdeq  28574  fusgr2wsp2nb  28599  hsn0elch  29511  eqsnd  30778  cycpmrn  31312  qsxpid  31460  prmidl0  31528  ccfldextdgrr  31644  xrge0iifiso  31787  qqhval2  31832  esumnul  31916  esumrnmpt2  31936  esumfzf  31937  sibfof  32207  sitgaddlemb  32215  plymulx0  32426  signstf0  32447  prodfzo03  32483  circlemeth  32520  bnj521  32616  sconnpi1  33101  dffr5  33627  eqfunresadj  33641  elima4  33656  xpord2pred  33719  xpord3pred  33725  ssltleft  33981  ssltright  33982  cofcutr  34019  brsingle  34146  dfiota3  34152  funpartfun  34172  dfrdg4  34180  fwddifn0  34393  bj-csbsnlem  35015  bj-pw0ALT  35149  bj-restsn  35180  bj-rest10  35186  mptsnunlem  35436  fvineqsneu  35509  matunitlindflem1  35700  poimirlem23  35727  poimirlem26  35730  poimirlem27  35731  grposnOLD  35967  0idl  36110  smprngopr  36137  isdmn3  36159  lshpdisj  36928  lsat0cv  36974  snatpsubN  37691  dibelval3  39088  dib1dim  39106  dvh2dim  39386  mapd0  39606  hdmap14lem13  39821  dvrelogpow2b  40004  sticksstones11  40040  sn-iotalem  40117  fnsnbt  40134  prjspeclsp  40372  pellexlem5  40571  jm2.23  40734  flcidc  40915  snhesn  41283  snssiALTVD  42336  snssiALT  42337  fsneq  42635  iccintsng  42951  icoiccdif  42952  limcrecl  43060  lptioo2  43062  lptioo1  43063  limcresiooub  43073  limcresioolb  43074  cnrefiisplem  43260  icccncfext  43318  dvmptfprodlem  43375  dvnprodlem3  43379  dirkercncflem2  43535  fourierdlem40  43578  fourierdlem48  43585  fourierdlem51  43588  fourierdlem62  43599  fourierdlem66  43603  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fourierdlem79  43616  fourierdlem93  43630  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  elaa2  43665  etransclem44  43709  rrxsnicc  43731  sge00  43804  absnsb  44408  funressnfv  44424  fsetsniunop  44430  dfdfat2  44507  tz6.12-afv  44552  tz6.12-afv2  44619  otiunsndisjX  44658  iccpartgtl  44766  iccpartgt  44767  iccpartleu  44768  iccpartgel  44769  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  bgoldbtbnd  45149  xpsnopab  45207  opeliun2xp  45556  mo0sn  46049  aacllem  46391