Theorem velsn 4610

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

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-sn 4595

This theorem is referenced by:  rabsneq  4613  dfpr2  4615  ralsnsg  4641  rexsns  4642  ralsng  4646  disjsn  4682  snprc  4688  snssb  4753  raldifsnb  4768  difprsnss  4771  pwpw0  4783  eqsn  4799  snsspw  4813  dfnfc2  4898  uni0b  4903  uni0c  4904  iunid  5029  iunsn  5034  rext  5430  moabexOLD  5441  exss  5445  otiunsndisj  5504  dffr6  5618  fconstmpt  5724  opeliunxp  5729  opeliun2xp  5730  rnep  5918  restidsing  6056  xpdifid  6166  dmsnopg  6215  sniota  6528  dfmpt3  6670  tz6.12-2  6869  nfunsn  6921  fnsnfv  6961  dffv2  6977  fsneq  7031  fsn  7132  fnasrn  7142  fnsnbg  7163  fnsnbOLD  7165  fmptsng  7167  fmptsnd  7168  fvclss  7240  eqfunresadj  7359  eusvobj2  7403  resf1extb  7931  opabex3d  7962  opabex3rd  7963  opabex3  7964  xpord2pred  8141  xpord3pred  8148  frrlem12  8294  frrlem13  8295  oarec  8547  mapdm0  8839  ixp0x  8924  snmapen  9035  xpsnen  9049  marypha2lem2  9396  elirrvOLDOLD  9561  cantnfp1lem1  9647  cantnfp1lem3  9649  djuunxp  9907  dfac5lem1  10107  dfac5lem2  10108  dfac5lem4  10110  fin1a2lem11  10394  axdc4lem  10439  axcclem  10441  ttukeylem7  10499  xrsupexmnf  13331  xrinfmexpnf  13332  iccid  13417  fzsn  13594  fzpr  13607  seqz  14086  hashf1  14494  pr2pwpr  14516  s3iunsndisj  15005  fsum2dlem  15821  incexc2  15892  prodsn  16016  prodsnf  16018  fprod2dlem  16034  ef0lem  16132  lcmfunsnlem2  16698  1nprm  16737  vdwapun  17034  prmodvdslcmf  17107  cshwsiun  17159  chnccat  18682  mgmidsssn0  18730  mnd1id  18838  0subm  18876  efmnd1bas  18952  smndex1basss  18967  smndex1mgm  18969  trivsubgsnd  19220  qsxpid  19243  kerf1ghm  19317  ghmqusnsglem1  19350  ghmquskerlem1  19353  ghmqusker  19357  symg1bas  19461  pmtrprfvalrn  19558  gex1  19661  sylow2alem1  19687  lsmdisj2  19752  0frgp  19849  0cyg  19963  prmcyg  19964  dprddisj2  20111  ablfacrp  20138  lspdisj  21227  lidlnz  21350  prmidl0  21447  mulgrhm2  21597  pzriprnglem10  21609  ocvin  21793  psrlidm  22080  mplcoe1  22157  mplcoe5  22160  psdmul  22298  maducoeval2  22766  madugsum  22769  en2top  23111  restsn  23296  ist1-3  23475  ordtt1  23505  cmpcld  23528  unisngl  23653  dissnlocfin  23655  ptopn2  23710  snfil  23990  alexsubALTlem2  24174  alexsubALTlem3  24175  alexsubALTlem4  24176  haustsms2  24263  tsmsxplem1  24279  tsmsxplem2  24280  ust0  24346  dscopn  24699  nmoid  24868  limcdif  26004  ellimc2  26005  limcmpt  26011  limcres  26014  ply1remlem  26291  plyeq0lem  26336  plyn0mulidp  26411  plyremlem  26434  aaliou2  26470  radcnv0  26545  abelthlem2  26561  wilthlem2  27199  vmappw  27246  ppinprm  27282  chtnprm  27284  musumsum  27322  dchrhash  27401  lgsquadlem1  27510  lgsquadlem2  27511  eqcuts3  27963  sltsleft  28019  sltsright  28020  cofcutr  28083  addsuniflem  28160  negsid  28200  negsunif  28214  sltmuls1  28306  sltmuls2  28307  precsexlem11  28376  oncutlt  28423  n0fincut  28514  elreno2  28654  cplgr1v  29721  rusgrnumwwlkb0  30264  frgrncvvdeq  30601  fusgr2wsp2nb  30626  hsn0elch  31541  indsn  33124  cycpmrn  33404  mvrvalind  33873  mplmonprod  33889  esplyfvaln  33909  esplyind  33910  ccfldextdgrr  34007  xrge0iifiso  34270  qqhval2  34317  esumnul  34383  esumrnmpt2  34403  esumfzf  34404  sibfof  34675  sitgaddlemb  34683  signstf0  34900  prodfzo03  34935  circlemeth  34972  scottsn  35454  kard0  35500  sconnpi1  35664  dffr5  36179  elima4  36201  brsingle  36340  dfiota3  36346  funpartfun  36368  dfrdg4  36376  fwddifn0  36589  mh-infprim2bi  36981  mh-infprim3bi  36982  bj-csbsnlem  37461  bj-axsn  37590  bj-axadj  37599  bj-pw0ALT  37607  bj-restsn  37646  bj-rest10  37652  mptsnunlem  37906  fvineqsneu  37979  matunitlindflem1  38189  poimirlem23  38216  poimirlem26  38219  poimirlem27  38220  grposnOLD  38455  0idl  38598  smprngopr  38625  isdmn3  38647  dfsucmap3  39036  ressn2  39105  lshpdisj  39685  lsat0cv  39731  snatpsubN  40448  dibelval3  41845  dib1dim  41863  dvh2dim  42143  mapd0  42363  hdmap14lem13  42578  dvrelogpow2b  42759  sticksstones11  42847  unitscyglem4  42889  sn-iotalem  42916  prjspeclsp  43270  pellexlem5  43486  jm2.23  43649  flcidc  43823  tfsconcatrn  43995  snhesn  44438  snssiALTVD  45461  snssiALT  45462  permaxinf2lem  45647  iccintsng  46165  icoiccdif  46166  limcrecl  46271  lptioo2  46273  lptioo1  46274  limcresiooub  46282  limcresioolb  46283  cnrefiisplem  46469  icccncfext  46527  dvmptfprodlem  46584  dvnprodlem3  46588  dirkercncflem2  46744  fourierdlem40  46787  fourierdlem48  46794  fourierdlem51  46797  fourierdlem62  46808  fourierdlem66  46812  fourierdlem74  46820  fourierdlem75  46821  fourierdlem76  46822  fourierdlem78  46824  fourierdlem79  46825  fourierdlem93  46839  fourierdlem101  46847  fourierdlem103  46849  fourierdlem104  46850  fouriersw  46871  elaa2  46874  etransclem44  46918  rrxsnicc  46940  sge00  47016  chnsubseq  47522  absnsb  47687  funressnfv  47703  fsetsniunop  47709  dfdfat2  47788  tz6.12-afv  47833  tz6.12-afv2  47900  otiunsndisjX  47939  iccpartgtl  48098  iccpartgt  48099  iccpartleu  48100  iccpartgel  48101  nnsum4primeseven  48488  nnsum4primesevenALTV  48489  bgoldbtbnd  48497  dfclnbgr6  48544  dfnbgr6  48545  stgredgiun  48646  xpsnopab  48845  smprngprmrng  49027  mo0sn  49513  tposres0  49574  setcsnterm  50187  2arwcatlem1  50292  2arwcat  50297  setc1onsubc  50299  aacllem  50509