Theorem velsn 4617

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  {csn 4601

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-sn 4602

This theorem is referenced by:  rabsneq  4620  dfpr2  4622  ralsnsg  4646  rexsns  4647  ralsng  4651  disjsn  4687  snprc  4693  snssb  4758  snssgOLD  4760  raldifsnb  4772  difprsnss  4775  pwpw0  4789  eqsn  4805  eqsndOLD  4807  snsspw  4820  dfnfc2  4905  uni0b  4909  uni0c  4910  iunid  5036  iunsn  5042  sndisj  5111  rext  5423  moabex  5434  exss  5438  otiunsndisj  5495  dffr6  5609  fconstmpt  5716  opeliunxp  5721  opeliun2xp  5722  rnep  5906  restidsing  6040  xpdifid  6157  dmsnopg  6202  sniota  6521  dfmpt3  6671  nfunsn  6917  fnsnfv  6957  dffv2  6973  fsn  7124  fnasrn  7134  fnsnbg  7155  fnsnbOLD  7157  fmptsng  7159  fmptsnd  7160  fvclss  7232  eqfunresadj  7352  eusvobj2  7395  sucexeloniOLD  7802  suceloniOLD  7804  resf1extb  7928  opabex3d  7962  opabex3rd  7963  opabex3  7964  xpord2pred  8142  xpord3pred  8149  frrlem12  8294  frrlem13  8295  wfrlem14OLD  8334  wfrlem15OLD  8335  oarec  8572  mapdm0  8854  ixp0x  8938  snmapen  9050  xpsnen  9067  marypha2lem2  9446  elirrv  9608  cantnfp1lem1  9690  cantnfp1lem3  9692  djuunxp  9933  dfac5lem1  10135  dfac5lem2  10136  dfac5lem4  10138  dfac5lem4OLD  10140  fin1a2lem11  10422  axdc4lem  10467  axcclem  10469  ttukeylem7  10527  xrsupexmnf  13319  xrinfmexpnf  13320  iccid  13405  fzsn  13581  fzpr  13594  seqz  14066  hashf1  14473  pr2pwpr  14495  s3iunsndisj  14985  fsum2dlem  15784  incexc2  15852  prodsn  15976  prodsnf  15978  fprod2dlem  15994  ef0lem  16092  lcmfunsnlem2  16657  1nprm  16696  vdwapun  16992  prmodvdslcmf  17065  cshwsiun  17117  mgmidsssn0  18648  mnd1id  18756  0subm  18793  efmnd1bas  18869  smndex1basss  18881  smndex1mgm  18883  trivsubgsnd  19135  kerf1ghm  19228  ghmqusnsglem1  19261  ghmquskerlem1  19264  ghmqusker  19268  symg1bas  19370  pmtrprfvalrn  19467  gex1  19570  sylow2alem1  19596  lsmdisj2  19661  0frgp  19758  0cyg  19872  prmcyg  19873  dprddisj2  20020  ablfacrp  20047  lspdisj  21084  lidlnz  21201  mulgrhm2  21437  pzriprnglem10  21449  ocvin  21632  psrlidm  21920  mplcoe1  21993  mplcoe5  21996  psdmul  22102  maducoeval2  22576  madugsum  22579  en2top  22921  restsn  23106  ist1-3  23285  ordtt1  23315  cmpcld  23338  unisngl  23463  dissnlocfin  23465  ptopn2  23520  snfil  23800  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALTlem4  23986  haustsms2  24073  tsmsxplem1  24089  tsmsxplem2  24090  ust0  24156  dscopn  24510  nmoid  24679  limcdif  25827  ellimc2  25828  limcmpt  25834  limcres  25837  ply1remlem  26120  plyeq0lem  26165  plyremlem  26262  aaliou2  26298  radcnv0  26375  abelthlem2  26392  wilthlem2  27029  vmappw  27076  ppinprm  27112  chtnprm  27114  musumsum  27152  dchrhash  27232  lgsquadlem1  27341  lgsquadlem2  27342  ssltsn  27754  ssltleft  27826  ssltright  27827  cofcutr  27875  addsuniflem  27951  negsid  27990  negsunif  28004  ssltmul1  28090  ssltmul2  28091  precsexlem11  28158  nohalf  28324  0reno  28346  cplgr1v  29355  rusgrnumwwlkb0  29899  frgrncvvdeq  30236  fusgr2wsp2nb  30261  hsn0elch  31175  cycpmrn  33100  qsxpid  33323  prmidl0  33411  ccfldextdgrr  33659  xrge0iifiso  33912  qqhval2  33959  esumnul  34025  esumrnmpt2  34045  esumfzf  34046  sibfof  34318  sitgaddlemb  34326  plymulx0  34525  signstf0  34546  prodfzo03  34581  circlemeth  34618  sconnpi1  35207  dffr5  35717  elima4  35739  brsingle  35881  dfiota3  35887  funpartfun  35907  dfrdg4  35915  fwddifn0  36128  bj-csbsnlem  36867  bj-axsn  36996  bj-axadj  37005  bj-pw0ALT  37013  bj-restsn  37046  bj-rest10  37052  mptsnunlem  37302  fvineqsneu  37375  matunitlindflem1  37586  poimirlem23  37613  poimirlem26  37616  poimirlem27  37617  grposnOLD  37852  0idl  37995  smprngopr  38022  isdmn3  38044  ressn2  38406  lshpdisj  38951  lsat0cv  38997  snatpsubN  39715  dibelval3  41112  dib1dim  41130  dvh2dim  41410  mapd0  41630  hdmap14lem13  41845  dvrelogpow2b  42027  sticksstones11  42115  unitscyglem4  42157  sn-iotalem  42218  prjspeclsp  42582  pellexlem5  42803  jm2.23  42967  flcidc  43141  tfsconcatrn  43313  snhesn  43757  snssiALTVD  44799  snssiALT  44800  permaxinf2lem  44985  fsneq  45178  iccintsng  45500  icoiccdif  45501  limcrecl  45606  lptioo2  45608  lptioo1  45609  limcresiooub  45619  limcresioolb  45620  cnrefiisplem  45806  icccncfext  45864  dvmptfprodlem  45921  dvnprodlem3  45925  dirkercncflem2  46081  fourierdlem40  46124  fourierdlem48  46131  fourierdlem51  46134  fourierdlem62  46145  fourierdlem66  46149  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem78  46161  fourierdlem79  46162  fourierdlem93  46176  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fouriersw  46208  elaa2  46211  etransclem44  46255  rrxsnicc  46277  sge00  46353  absnsb  47004  funressnfv  47020  fsetsniunop  47026  dfdfat2  47105  tz6.12-afv  47150  tz6.12-afv2  47217  otiunsndisjX  47256  iccpartgtl  47388  iccpartgt  47389  iccpartleu  47390  iccpartgel  47391  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbtbnd  47771  dfclnbgr6  47817  dfnbgr6  47818  stgredgiun  47918  xpsnopab  48080  mo0sn  48742  tposres0  48800  setcsnterm  49323  2arwcatlem1  49420  2arwcat  49425  setc1onsubc  49427  aacllem  49613