Theorem velsn 4451

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

Syntax hints:   ↔ wb 198   = wceq 1508   ∈ wcel 2051  {csn 4435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-v 3410  df-sn 4436

This theorem is referenced by:  dfpr2  4454  ralsnsg  4476  rexsns  4477  disjsn  4517  snprc  4523  snssg  4587  raldifsnb  4599  difprsnss  4602  pwpw0  4616  eqsn  4632  snsspw  4645  pwsnALT  4701  dfnfc2  4726  uni0b  4733  uni0c  4734  sndisj  4917  rext  5193  moabex  5204  exss  5208  otiunsndisj  5262  fconstmpt  5460  opeliunxp  5465  restidsing  5761  xpdifid  5862  dmsnopg  5906  sniota  6176  dfmpt3  6309  nfunsn  6534  dffv2  6582  fsn  6718  fnasrn  6728  fnsnb  6749  fmptsng  6751  fmptsnd  6752  fvclss  6824  eusvobj2  6967  suceloni  7342  opabex3d  7476  opabex3rd  7477  opabex3  7478  wfrlem14  7770  wfrlem15  7771  oarec  7987  mapdm0  8219  ixp0x  8285  snmapen  8385  xpsnen  8395  marypha2lem2  8693  elirrv  8853  cantnfp1lem1  8933  cantnfp1lem3  8935  djuunxp  9142  dfac5lem1  9341  dfac5lem2  9342  dfac5lem4  9344  fin1a2lem11  9628  axdc4lem  9673  axcclem  9675  ttukeylem7  9733  xrsupexmnf  12512  xrinfmexpnf  12513  iccid  12597  fzsn  12763  fzpr  12776  seqz  13231  hashf1  13626  pr2pwpr  13646  s3iunsndisj  14187  fsum2dlem  14983  incexc2  15051  prodsn  15174  prodsnf  15176  fprod2dlem  15192  ef0lem  15290  lcmfunsnlem2  15838  1nprm  15877  vdwapun  16164  prmodvdslcmf  16237  cshwsiun  16287  xpsc0  16689  xpsc1  16690  mgmidsssn0  17749  mnd1id  17812  symg1bas  18297  pmtrprfvalrn  18389  gex1  18489  sylow2alem1  18515  lsmdisj2  18578  0frgp  18677  0cyg  18779  prmcyg  18780  dprddisj2  18923  ablfacrp  18950  kerf1ghm  19232  kerf1hrmOLD  19233  lspdisj  19631  lidlnz  19734  psrlidm  19909  mplcoe1  19971  mplcoe5  19974  evlslem1  20020  mulgrhm2  20363  ocvin  20535  maducoeval2  20968  madugsum  20971  en2top  21312  restsn  21497  ist1-3  21676  ordtt1  21706  cmpcld  21729  unisngl  21854  dissnlocfin  21856  ptopn2  21911  snfil  22191  alexsubALTlem2  22375  alexsubALTlem3  22376  alexsubALTlem4  22377  haustsms2  22463  tsmsxplem1  22479  tsmsxplem2  22480  ust0  22546  dscopn  22901  nmoid  23069  limcdif  24192  ellimc2  24193  limcmpt  24199  limcres  24202  ply1remlem  24474  plyeq0lem  24518  plyremlem  24611  aaliou2  24647  radcnv0  24722  abelthlem2  24738  wilthlem2  25363  vmappw  25410  ppinprm  25446  chtnprm  25448  musumsum  25486  dchrhash  25564  lgsquadlem1  25673  lgsquadlem2  25674  cplgr1v  26930  rusgrnumwwlkb0  27492  frgrncvvdeq  27858  fusgr2wsp2nb  27883  hsn0elch  28819  eqsnd  30078  ccfldextdgrr  30718  xrge0iifiso  30854  qqhval2  30899  esumnul  30983  esumrnmpt2  31003  esumfzf  31004  sibfof  31275  sitgaddlemb  31283  plymulx0  31495  signstf0  31516  signstfvneq0  31521  prodfzo03  31554  circlemeth  31591  bnj521  31687  sconnpi1  32108  dffr5  32546  eqfunresadj  32561  elima4  32576  frrlem12  32692  frrlem13  32693  brsingle  32936  dfiota3  32942  funpartfun  32962  dfrdg4  32970  fwddifn0  33183  bj-csbsnlem  33749  bj-restsn  33920  bj-rest10  33926  mptsnunlem  34098  fvineqsneu  34170  matunitlindflem1  34366  poimirlem23  34393  poimirlem26  34396  poimirlem27  34397  grposnOLD  34639  0idl  34782  smprngopr  34809  isdmn3  34831  lshpdisj  35605  lsat0cv  35651  snatpsubN  36368  dibelval3  37765  dib1dim  37783  dvh2dim  38063  mapd0  38283  hdmap14lem13  38498  iunsn  38601  fnsnbt  38603  prjspeclsp  38707  pellexlem5  38864  jm2.23  39027  flcidc  39208  snhesn  39533  trivsubgd2  40052  snssiALTVD  40618  snssiALT  40619  fsneq  40929  iccintsng  41264  icoiccdif  41265  limcrecl  41375  lptioo2  41377  lptioo1  41378  limcresiooub  41388  limcresioolb  41389  cnrefiisplem  41575  icccncfext  41634  dvmptfprodlem  41693  dvnprodlem3  41697  dirkercncflem2  41854  fourierdlem40  41897  fourierdlem48  41904  fourierdlem51  41907  fourierdlem62  41918  fourierdlem66  41922  fourierdlem74  41930  fourierdlem75  41931  fourierdlem76  41932  fourierdlem78  41934  fourierdlem79  41935  fourierdlem93  41949  fourierdlem101  41957  fourierdlem103  41959  fourierdlem104  41960  fouriersw  41981  elaa2  41984  etransclem44  42028  rrxsnicc  42050  sge00  42123  absnsb  42701  funressnfv  42717  dfdfat2  42767  tz6.12-afv  42812  tz6.12-afv2  42879  otiunsndisjX  42918  iccpartgtl  42992  iccpartgt  42993  iccpartleu  42994  iccpartgel  42995  nnsum4primeseven  43367  nnsum4primesevenALTV  43368  bgoldbtbnd  43376  xpsnopab  43434  opeliun2xp  43779  aacllem  44303