Theorem elsn 3382

Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
elsn	⊢ (x ∈ {A} ↔ x = A)

Distinct variable group:   x,A

Proof of Theorem elsn

Step	Hyp	Ref	Expression
1		df-sn 3373	. 2 ⊢ {A} = {x ∣ x = A}
2	1	abeq2i 2145	1 ⊢ (x ∈ {A} ↔ x = A)

Syntax hints:   ↔ wb 98   = wceq 1242   ∈ wcel 1390  {csn 3367

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-sn 3373

This theorem is referenced by:  dfpr2  3383  mosn  3398  ralsns  3399  rexsns  3400  rexsnsOLD  3401  disjsn  3423  snprc  3426  euabsn2  3430  prmg  3480  snss  3485  difprsnss  3493  eqsnm  3517  snsssn  3523  snsspw  3526  dfnfc2  3589  uni0b  3596  uni0c  3597  sndisj  3751  unidif0  3911  rext  3942  exss  3954  ordsucim  4192  ordtriexmidlem  4208  onsucelsucexmidlem  4214  elirr  4224  sucprcreg  4227  fconstmpt  4330  opeliunxp  4338  dmsnopg  4735  dfmpt3  4964  nfunsn  5150  fsn  5278  fnasrn  5284  fnasrng  5286  fconstfvm  5322  eusvobj2  5441  opabex3d  5690  opabex3  5691  ecexr  6047  xpsnen  6231  iccid  8544  fzsn  8679  fzpr  8689  fzdifsuc  8693