Theorem velsn 4599

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {csn 4583

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sn 4584

This theorem is used by:  rabsneq  4602  dfpr2  4604  ralsnsg  4630  rexsns  4631  ralsng  4635  disjsn  4671  snprc  4677  snssb  4742  raldifsnb  4758  difprsnss  4761  pwpw0  4773  eqsn  4789  snsspw  4803  dfnfc2  4888  uni0b  4893  uni0c  4894  iunid  5018  iunsn  5023  rext  5415  moabexOLD  5426  exss  5430  otiunsndisj  5492  dffr6  5606  fconstmpt  5712  opeliunxp  5717  opeliun2xp  5718  rnep  5908  restidsing  6044  xpdifid  6158  dmsnopg  6214  sniota  6529  dfmpt3  6673  tz6.12-2  6872  nfunsn  6924  fnsnfv  6964  dffv2  6980  fsneq  7034  fsn  7136  fnasrn  7148  fnsnbg  7169  fnsnbOLD  7171  fmptsng  7173  fmptsnd  7174  fvclss  7245  eqfunresadj  7370  eusvobj2  7412  resf1extb  7946  opabex3d  7977  opabex3rd  7978  opabex3  7979  xpord2pred  8162  xpord3pred  8169  frrlem12  8315  frrlem13  8316  oarec  8570  mapdm0  8862  ixp0x  8954  snmapen  9066  xpsnen  9080  marypha2lem2  9428  elirrvOLDOLD  9593  cantnfp1lem1  9679  cantnfp1lem3  9681  djuunxp  10002  dfac5lem1  10202  dfac5lem2  10203  dfac5lem4  10205  fin1a2lem11  10488  axdc4lem  10533  axcclem  10535  ttukeylem7  10593  xrsupexmnf  13435  xrinfmexpnf  13436  iccid  13521  fzsn  13700  fzpr  13713  seqz  14193  hashf1  14602  pr2pwpr  14624  s3iunsndisj  15121  fsum2dlem  15936  incexc2  16007  prodsn  16129  prodsnf  16131  fprod2dlem  16147  ef0lem  16244  lcmfunsnlem2  16815  1nprm  16854  vdwapun  17152  prmodvdslcmf  17225  cshwsiun  17277  chnccat  18800  mgmidsssn0  18853  mnd1id  18974  0subm  19013  efmnd1bas  19089  smndex1basss  19104  smndex1mgm  19106  trivsubgsnd  19364  qsxpid  19387  kerf1ghm  19461  ghmqusnsglem1  19494  ghmquskerlem1  19497  ghmqusker  19501  symg1bas  19605  pmtrprfvalrn  19702  gex1  19805  sylow2alem1  19831  lsmdisj2  19896  0frgp  19993  0cyg  20107  prmcyg  20108  dprddisj2  20255  ablfacrp  20282  lspdisj  21403  lidlnz  21530  prmidl0  21634  mulgrhm2  21784  pzriprnglem10  21796  ocvin  21980  psrlidm  22269  mplcoe1  22346  mplcoe5  22349  psdmul  22487  maducoeval2  22955  madugsum  22958  matunitlindflem1  22994  en2top  23303  restsn  23488  ist1-3  23667  ordtt1  23697  cmpcld  23720  unisngl  23846  dissnlocfin  23848  ptopn2  23903  snfil  24183  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALTlem4  24369  haustsms2  24456  tsmsxplem1  24472  tsmsxplem2  24473  ust0  24539  dscopn  24892  nmoid  25061  limcdif  26196  ellimc2  26197  limcmpt  26203  limcres  26206  ply1remlem  26483  plyeq0lem  26529  plyn0mulidp  26602  plyremlem  26625  aaliou2  26667  radcnv0  26743  abelthlem2  26759  wilthlem2  27396  vmappw  27443  ppinprm  27479  chtnprm  27481  musumsum  27519  dchrhash  27598  lgsquadlem1  27707  lgsquadlem2  27708  eqcuts3  28190  sltsleft  28246  sltsright  28247  cofcutr  28310  addsuniflem  28387  negsid  28427  negsunif  28441  sltmuls1  28533  sltmuls2  28534  precsexlem11  28603  oncutlt  28650  n0fincut  28741  elreno2  28881  cplgr1v  30011  rusgrnumwwlkb0  30563  frgrncvvdeq  30910  fusgr2wsp2nb  30935  hsn0elch  31850  indsn  33430  cycpmrn  33704  mvrvalind  34170  mplmonprod  34186  esplyfvaln  34206  esplyind  34207  ccfldextdgrr  34304  xrge0iifiso  34567  qqhval2  34614  esumnul  34680  esumrnmpt2  34700  esumfzf  34701  sibfof  34972  sitgaddlemb  34980  signstf0  35197  prodfzo03  35232  circlemeth  35269  scottsn  35750  kard0  35822  sconnpi1  36004  elima4  36540  brsingle  36679  dfiota3  36685  funpartfun  36707  dfrdg4  36715  fwddifn0  36929  mh-infprim2bi  37335  mh-infprim3bi  37336  bj-csbsnlem  37815  bj-axsn  37945  bj-axadj  37954  bj-pw0ALT  37964  bj-restsn  38003  bj-rest10  38009  mptsnunlem  38262  fvineqsneu  38335  poimirlem23  38562  poimirlem26  38565  poimirlem27  38566  negprop  38644  grposnOLD  38817  0idl  38960  smprngopr  38987  isdmn3  39009  dfsucmap3  39396  ressn2  39465  lshpdisj  40045  lsat0cv  40091  snatpsubN  40808  dibelval3  42205  dib1dim  42223  dvh2dim  42503  mapd0  42723  hdmap14lem13  42938  dvrelogpow2b  43119  sticksstones11  43207  unitscyglem4  43249  sn-iotalem  43276  prjspeclsp  43641  pellexlem5  43840  jm2.23  44003  flcidc  44172  tfsconcatrn  44344  snhesn  44786  snssiALTVD  45809  snssiALT  45810  permaxinf2lem  46002  iccintsng  46535  icoiccdif  46536  limcrecl  46641  lptioo2  46643  lptioo1  46644  limcresiooub  46652  limcresioolb  46653  cnrefiisplem  46839  icccncfext  46897  dvmptfprodlem  46954  dvnprodlem3  46958  dirkercncflem2  47114  fourierdlem40  47157  fourierdlem48  47164  fourierdlem51  47167  fourierdlem62  47178  fourierdlem66  47182  fourierdlem74  47190  fourierdlem75  47191  fourierdlem76  47192  fourierdlem78  47194  fourierdlem79  47195  fourierdlem93  47209  fourierdlem101  47217  fourierdlem103  47219  fourierdlem104  47220  fouriersw  47241  elaa2  47244  etransclem44  47288  rrxsnicc  47310  sge00  47386  absnsb  48097  funressnfv  48113  fsetsniunop  48119  dfdfat2  48198  tz6.12-afv  48243  tz6.12-afv2  48310  otiunsndisjX  48349  iccpartgtl  48508  iccpartgt  48509  iccpartleu  48510  iccpartgel  48511  nnsum4primeseven  48898  nnsum4primesevenALTV  48899  bgoldbtbnd  48907  dfclnbgr6  48954  dfnbgr6  48955  stgredgiun  49056  xpsnopab  49255  smprngprmrng  49436  isidom3  49442  mo0sn  49926  tposres0  49985  setcsnterm  50598  2arwcatlem1  50703  2arwcat  50708  setc1onsubc  50710  aacllem  50939