Theorem velsn 4645

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2104  {csn 4629

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-sn 4630

This theorem is referenced by:  dfpr2  4648  ralsnsg  4673  rexsns  4674  ralsng  4678  disjsn  4716  snprc  4722  snssb  4787  snssgOLD  4789  raldifsnb  4800  difprsnss  4803  pwpw0  4817  eqsn  4833  snsspw  4846  pwsnOLD  4902  dfnfc2  4934  uni0b  4938  uni0c  4939  iunid  5064  iunsn  5070  sndisj  5140  rext  5449  moabex  5460  exss  5464  otiunsndisj  5521  dffr6  5635  fconstmpt  5739  opeliunxp  5744  rnep  5927  restidsing  6053  xpdifid  6168  dmsnopg  6213  sniota  6535  dfmpt3  6685  nfunsn  6934  fnsnfv  6971  dffv2  6987  fsn  7136  fnasrn  7146  fnsnb  7167  fmptsng  7169  fmptsnd  7170  fvclss  7244  eqfunresadj  7361  eusvobj2  7405  sucexeloniOLD  7802  suceloniOLD  7804  opabex3d  7956  opabex3rd  7957  opabex3  7958  xpord2pred  8135  xpord3pred  8142  frrlem12  8286  frrlem13  8287  wfrlem14OLD  8326  wfrlem15OLD  8327  oarec  8566  mapdm0  8840  ixp0x  8924  snmapen  9042  xpsnen  9059  marypha2lem2  9435  elirrv  9595  cantnfp1lem1  9677  cantnfp1lem3  9679  djuunxp  9920  dfac5lem1  10122  dfac5lem2  10123  dfac5lem4  10125  fin1a2lem11  10409  axdc4lem  10454  axcclem  10456  ttukeylem7  10514  xrsupexmnf  13290  xrinfmexpnf  13291  iccid  13375  fzsn  13549  fzpr  13562  seqz  14022  hashf1  14424  pr2pwpr  14446  s3iunsndisj  14921  fsum2dlem  15722  incexc2  15790  prodsn  15912  prodsnf  15914  fprod2dlem  15930  ef0lem  16028  lcmfunsnlem2  16583  1nprm  16622  vdwapun  16913  prmodvdslcmf  16986  cshwsiun  17039  mgmidsssn0  18599  mnd1id  18704  0subm  18736  efmnd1bas  18812  smndex1basss  18824  smndex1mgm  18826  trivsubgsnd  19072  kerf1ghm  19163  symg1bas  19301  pmtrprfvalrn  19399  gex1  19502  sylow2alem1  19528  lsmdisj2  19593  0frgp  19690  0cyg  19804  prmcyg  19805  dprddisj2  19952  ablfacrp  19979  lspdisj  20885  lidlnz  21004  mulgrhm2  21251  pzriprnglem10  21261  ocvin  21448  psrlidm  21744  mplcoe1  21813  mplcoe5  21816  maducoeval2  22364  madugsum  22367  en2top  22710  restsn  22896  ist1-3  23075  ordtt1  23105  cmpcld  23128  unisngl  23253  dissnlocfin  23255  ptopn2  23310  snfil  23590  alexsubALTlem2  23774  alexsubALTlem3  23775  alexsubALTlem4  23776  haustsms2  23863  tsmsxplem1  23879  tsmsxplem2  23880  ust0  23946  dscopn  24304  nmoid  24481  limcdif  25627  ellimc2  25628  limcmpt  25634  limcres  25637  ply1remlem  25914  plyeq0lem  25958  plyremlem  26051  aaliou2  26087  radcnv0  26162  abelthlem2  26178  wilthlem2  26807  vmappw  26854  ppinprm  26890  chtnprm  26892  musumsum  26930  dchrhash  27008  lgsquadlem1  27117  lgsquadlem2  27118  ssltsn  27528  ssltleft  27600  ssltright  27601  cofcutr  27647  addsuniflem  27721  negsid  27752  negsunif  27766  ssltmul1  27839  ssltmul2  27840  precsexlem11  27900  cplgr1v  28952  rusgrnumwwlkb0  29490  frgrncvvdeq  29827  fusgr2wsp2nb  29852  hsn0elch  30766  eqsnd  32031  cycpmrn  32570  qsxpid  32746  ghmquskerlem1  32800  ghmqusker  32804  prmidl0  32841  ccfldextdgrr  33033  xrge0iifiso  33211  qqhval2  33258  esumnul  33342  esumrnmpt2  33362  esumfzf  33363  sibfof  33635  sitgaddlemb  33643  plymulx0  33854  signstf0  33875  prodfzo03  33911  circlemeth  33948  sconnpi1  34526  dffr5  35026  elima4  35049  brsingle  35191  dfiota3  35197  funpartfun  35217  dfrdg4  35225  fwddifn0  35438  bj-csbsnlem  36088  bj-axsn  36218  bj-axadj  36227  bj-pw0ALT  36235  bj-restsn  36268  bj-rest10  36274  mptsnunlem  36524  fvineqsneu  36597  matunitlindflem1  36789  poimirlem23  36816  poimirlem26  36819  poimirlem27  36820  grposnOLD  37055  0idl  37198  smprngopr  37225  isdmn3  37247  ressn2  37617  lshpdisj  38162  lsat0cv  38208  snatpsubN  38926  dibelval3  40323  dib1dim  40341  dvh2dim  40621  mapd0  40841  hdmap14lem13  41056  dvrelogpow2b  41241  sticksstones11  41280  sn-iotalem  41346  fnsnbt  41359  prjspeclsp  41658  pellexlem5  41875  jm2.23  42039  flcidc  42220  tfsconcatrn  42396  snhesn  42841  snssiALTVD  43892  snssiALT  43893  fsneq  44205  iccintsng  44536  icoiccdif  44537  limcrecl  44645  lptioo2  44647  lptioo1  44648  limcresiooub  44658  limcresioolb  44659  cnrefiisplem  44845  icccncfext  44903  dvmptfprodlem  44960  dvnprodlem3  44964  dirkercncflem2  45120  fourierdlem40  45163  fourierdlem48  45170  fourierdlem51  45173  fourierdlem62  45184  fourierdlem66  45188  fourierdlem74  45196  fourierdlem75  45197  fourierdlem76  45198  fourierdlem78  45200  fourierdlem79  45201  fourierdlem93  45215  fourierdlem101  45223  fourierdlem103  45225  fourierdlem104  45226  fouriersw  45247  elaa2  45250  etransclem44  45294  rrxsnicc  45316  sge00  45392  absnsb  46037  funressnfv  46053  fsetsniunop  46059  dfdfat2  46136  tz6.12-afv  46181  tz6.12-afv2  46248  otiunsndisjX  46287  iccpartgtl  46394  iccpartgt  46395  iccpartleu  46396  iccpartgel  46397  nnsum4primeseven  46768  nnsum4primesevenALTV  46769  bgoldbtbnd  46777  xpsnopab  46835  opeliun2xp  47098  mo0sn  47589  aacllem  47937