Theorem velsn 4193

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

Syntax hints:   ↔ wb 196   = wceq 1483   ∈ wcel 1990  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sn 4178

This theorem is referenced by:  dfpr2  4195  ralsnsg  4216  rexsns  4217  disjsn  4246  snprc  4253  euabsn2  4260  snss  4316  raldifsnb  4325  difprsnss  4329  pwpw0  4344  eqsn  4361  eqsnOLD  4362  snsspw  4375  pwsnALT  4429  dfnfc2  4454  dfnfc2OLD  4455  uni0b  4463  uni0c  4464  sndisj  4644  rext  4916  moabex  4927  exss  4931  otiunsndisj  4980  fconstmpt  5163  opeliunxp  5170  restidsing  5458  restidsingOLD  5459  xpdifid  5562  dmsnopg  5606  elsnxpOLD  5678  sniota  5878  dfmpt3  6014  nfunsn  6225  dffv2  6271  fsn  6402  fnasrn  6411  fnsnb  6432  fmptsng  6434  fmptsnd  6435  fvclss  6500  eusvobj2  6643  suceloni  7013  opabex3d  7145  opabex3  7146  wfrlem14  7428  wfrlem15  7429  oarec  7642  ixp0x  7936  xpsnen  8044  marypha2lem2  8342  elirrv  8504  cantnfp1lem1  8575  cantnfp1lem3  8577  dfac5lem1  8946  dfac5lem2  8947  dfac5lem4  8949  fin1a2lem11  9232  axdc4lem  9277  axcclem  9279  ttukeylem7  9337  xrsupexmnf  12135  xrinfmexpnf  12136  iccid  12220  fzsn  12383  fzpr  12396  seqz  12849  hashf1  13241  pr2pwpr  13261  s3iunsndisj  13707  fsum2dlem  14501  incexc2  14570  prodsn  14692  prodsnf  14694  fprod2dlem  14710  ef0lem  14809  divalgmodOLD  15130  lcmfunsnlem2  15353  1nprm  15392  vdwapun  15678  prmodvdslcmf  15751  cshwsiun  15806  xpsc0  16220  xpsc1  16221  mgmidsssn0  17269  mnd1id  17332  symg1bas  17816  pmtrprfvalrn  17908  gex1  18006  sylow2alem1  18032  lsmdisj2  18095  0frgp  18192  0cyg  18294  prmcyg  18295  dprddisj2  18438  ablfacrp  18465  kerf1hrm  18743  lspdisj  19125  lidlnz  19228  psrlidm  19403  mplcoe1  19465  mplcoe5  19468  evlslem1  19515  mulgrhm2  19847  ocvin  20018  maducoeval2  20446  madugsum  20449  en2top  20789  restsn  20974  ist1-3  21153  ordtt1  21183  cmpcld  21205  unisngl  21330  dissnlocfin  21332  ptopn2  21387  snfil  21668  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  haustsms2  21940  tsmsxplem1  21956  tsmsxplem2  21957  ust0  22023  dscopn  22378  nmoid  22546  limcdif  23640  ellimc2  23641  limcmpt  23647  limcres  23650  ply1remlem  23922  plyeq0lem  23966  plyremlem  24059  aaliou2  24095  radcnv0  24170  abelthlem2  24186  wilthlem2  24795  vmappw  24842  ppinprm  24878  chtnprm  24880  musumsum  24918  dchrhash  24996  lgsquadlem1  25105  lgsquadlem2  25106  cplgr1v  26326  rusgrnumwwlkb0  26866  frgrncvvdeq  27173  fusgr2wsp2nb  27198  hsn0elch  28105  xrge0iifiso  29981  qqhval2  30026  esumnul  30110  esumrnmpt2  30130  esumfzf  30131  sibfof  30402  sitgaddlemb  30410  plymulx0  30624  signstf0  30645  signstfvneq0  30649  prodfzo03  30681  circlemeth  30718  bnj145OLD  30795  bnj521  30805  sconnpi1  31221  dffr5  31643  eqfunresadj  31659  elima4  31679  brsingle  32024  dfiota3  32030  funpartfun  32050  dfrdg4  32058  fwddifn0  32271  bj-csbsnlem  32898  bj-restsn  33035  bj-rest10  33041  bj-raldifsn  33054  mptsnunlem  33185  matunitlindflem1  33405  poimirlem23  33432  poimirlem26  33435  poimirlem27  33436  grposnOLD  33681  0idl  33824  smprngopr  33851  isdmn3  33873  lshpdisj  34274  lsat0cv  34320  snatpsubN  35036  dibelval3  36436  dib1dim  36454  dvh2dim  36734  mapd0  36954  hdmap14lem13  37172  pellexlem5  37397  jm2.23  37563  flcidc  37744  snhesn  38080  snssiALTVD  39062  snssiALT  39063  fsneq  39398  iccintsng  39749  icoiccdif  39750  limcrecl  39861  lptioo2  39863  lptioo1  39864  limcresiooub  39874  limcresioolb  39875  cnrefiisplem  40055  icccncfext  40100  dvmptfprodlem  40159  dvnprodlem3  40163  dirkercncflem2  40321  fourierdlem40  40364  fourierdlem48  40371  fourierdlem51  40374  fourierdlem62  40385  fourierdlem66  40389  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem79  40402  fourierdlem93  40416  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fouriersw  40448  elaa2  40451  etransclem44  40495  rrxsnicc  40520  sge00  40593  funressnfv  41208  dfdfat2  41211  tz6.12-afv  41253  otiunsndisjX  41298  iccpartgtl  41362  iccpartgt  41363  iccpartleu  41364  iccpartgel  41365  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbnd  41697  xpsnopab  41765  opeliun2xp  42111  aacllem  42547