Theorem velsn 4597

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {csn 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-sn 4582

This theorem is referenced by:  rabsneq  4600  dfpr2  4602  ralsnsg  4628  rexsns  4629  ralsng  4633  disjsn  4669  snprc  4675  snssb  4740  raldifsnb  4753  difprsnss  4756  pwpw0  4770  eqsn  4786  eqsndOLD  4788  snsspw  4801  dfnfc2  4886  uni0b  4890  uni0c  4891  iunid  5017  iunsn  5022  sndisj  5091  rext  5397  moabexOLD  5408  exss  5412  otiunsndisj  5469  dffr6  5581  fconstmpt  5687  opeliunxp  5692  opeliun2xp  5693  rnep  5877  restidsing  6013  xpdifid  6127  dmsnopg  6172  sniota  6484  dfmpt3  6627  tz6.12-2  6822  nfunsn  6874  fnsnfv  6914  dffv2  6930  fsn  7082  fnasrn  7092  fnsnbg  7112  fnsnbOLD  7114  fmptsng  7116  fmptsnd  7117  fvclss  7189  eqfunresadj  7308  eusvobj2  7352  resf1extb  7878  opabex3d  7911  opabex3rd  7912  opabex3  7913  xpord2pred  8089  xpord3pred  8096  frrlem12  8241  frrlem13  8242  oarec  8491  mapdm0  8783  ixp0x  8868  snmapen  8979  xpsnen  8993  marypha2lem2  9343  elirrvOLD  9507  cantnfp1lem1  9591  cantnfp1lem3  9593  djuunxp  9837  dfac5lem1  10037  dfac5lem2  10038  dfac5lem4  10040  dfac5lem4OLD  10042  fin1a2lem11  10324  axdc4lem  10369  axcclem  10371  ttukeylem7  10429  xrsupexmnf  13224  xrinfmexpnf  13225  iccid  13310  fzsn  13486  fzpr  13499  seqz  13977  hashf1  14384  pr2pwpr  14406  s3iunsndisj  14895  fsum2dlem  15697  incexc2  15765  prodsn  15889  prodsnf  15891  fprod2dlem  15907  ef0lem  16005  lcmfunsnlem2  16571  1nprm  16610  vdwapun  16906  prmodvdslcmf  16979  cshwsiun  17031  chnccat  18553  mgmidsssn0  18601  mnd1id  18709  0subm  18746  efmnd1bas  18822  smndex1basss  18834  smndex1mgm  18836  trivsubgsnd  19087  kerf1ghm  19180  ghmqusnsglem1  19213  ghmquskerlem1  19216  ghmqusker  19220  symg1bas  19324  pmtrprfvalrn  19421  gex1  19524  sylow2alem1  19550  lsmdisj2  19615  0frgp  19712  0cyg  19826  prmcyg  19827  dprddisj2  19974  ablfacrp  20001  lspdisj  21084  lidlnz  21201  mulgrhm2  21437  pzriprnglem10  21449  ocvin  21633  psrlidm  21921  mplcoe1  21996  mplcoe5  21999  psdmul  22113  maducoeval2  22588  madugsum  22591  en2top  22933  restsn  23118  ist1-3  23297  ordtt1  23327  cmpcld  23350  unisngl  23475  dissnlocfin  23477  ptopn2  23532  snfil  23812  alexsubALTlem2  23996  alexsubALTlem3  23997  alexsubALTlem4  23998  haustsms2  24085  tsmsxplem1  24101  tsmsxplem2  24102  ust0  24168  dscopn  24521  nmoid  24690  limcdif  25837  ellimc2  25838  limcmpt  25844  limcres  25847  ply1remlem  26130  plyeq0lem  26175  plyremlem  26272  aaliou2  26308  radcnv0  26385  abelthlem2  26402  wilthlem2  27039  vmappw  27086  ppinprm  27122  chtnprm  27124  musumsum  27162  dchrhash  27242  lgsquadlem1  27351  lgsquadlem2  27352  eqcuts3  27804  sltsleft  27860  sltsright  27861  cofcutr  27924  addsuniflem  28001  negsid  28041  negsunif  28055  sltmuls1  28147  sltmuls2  28148  precsexlem11  28217  oncutlt  28264  n0fincut  28355  elreno2  28495  cplgr1v  29507  rusgrnumwwlkb0  30051  frgrncvvdeq  30388  fusgr2wsp2nb  30413  hsn0elch  31327  indsn  32947  cycpmrn  33227  qsxpid  33445  prmidl0  33533  mvrvalind  33705  esplyind  33733  ccfldextdgrr  33831  xrge0iifiso  34094  qqhval2  34141  esumnul  34207  esumrnmpt2  34227  esumfzf  34228  sibfof  34499  sitgaddlemb  34507  plymulx0  34706  signstf0  34727  prodfzo03  34762  circlemeth  34799  sconnpi1  35435  dffr5  35950  elima4  35972  brsingle  36111  dfiota3  36117  funpartfun  36139  dfrdg4  36147  fwddifn0  36360  bj-csbsnlem  37106  bj-axsn  37235  bj-axadj  37244  bj-pw0ALT  37252  bj-restsn  37289  bj-rest10  37295  mptsnunlem  37545  fvineqsneu  37618  matunitlindflem1  37819  poimirlem23  37846  poimirlem26  37849  poimirlem27  37850  grposnOLD  38085  0idl  38228  smprngopr  38255  isdmn3  38277  dfsucmap3  38666  ressn2  38735  lshpdisj  39315  lsat0cv  39361  snatpsubN  40078  dibelval3  41475  dib1dim  41493  dvh2dim  41773  mapd0  41993  hdmap14lem13  42208  dvrelogpow2b  42390  sticksstones11  42478  unitscyglem4  42520  sn-iotalem  42545  prjspeclsp  42922  pellexlem5  43142  jm2.23  43305  flcidc  43479  tfsconcatrn  43651  snhesn  44094  snssiALTVD  45134  snssiALT  45135  permaxinf2lem  45320  fsneq  45517  iccintsng  45836  icoiccdif  45837  limcrecl  45942  lptioo2  45944  lptioo1  45945  limcresiooub  45953  limcresioolb  45954  cnrefiisplem  46140  icccncfext  46198  dvmptfprodlem  46255  dvnprodlem3  46259  dirkercncflem2  46415  fourierdlem40  46458  fourierdlem48  46465  fourierdlem51  46468  fourierdlem62  46479  fourierdlem66  46483  fourierdlem74  46491  fourierdlem75  46492  fourierdlem76  46493  fourierdlem78  46495  fourierdlem79  46496  fourierdlem93  46510  fourierdlem101  46518  fourierdlem103  46520  fourierdlem104  46521  fouriersw  46542  elaa2  46545  etransclem44  46589  rrxsnicc  46611  sge00  46687  chnsubseq  47191  absnsb  47340  funressnfv  47356  fsetsniunop  47362  dfdfat2  47441  tz6.12-afv  47486  tz6.12-afv2  47553  otiunsndisjX  47592  iccpartgtl  47739  iccpartgt  47740  iccpartleu  47741  iccpartgel  47742  nnsum4primeseven  48113  nnsum4primesevenALTV  48114  bgoldbtbnd  48122  dfclnbgr6  48169  dfnbgr6  48170  stgredgiun  48271  xpsnopab  48470  mo0sn  49128  tposres0  49189  setcsnterm  49802  2arwcatlem1  49907  2arwcat  49912  setc1onsubc  49914  aacllem  50113