ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  velsn Unicode version

Theorem velsn 3608
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  |-  ( x  e.  { A }  <->  x  =  A )

Proof of Theorem velsn
StepHypRef Expression
1 vex 2740 . 2  |-  x  e. 
_V
21elsn 3607 1  |-  ( x  e.  { A }  <->  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 105    = wceq 1353    e. wcel 2148   {csn 3591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-sn 3597
This theorem is referenced by:  dfpr2  3610  mosn  3627  ralsnsg  3628  ralsns  3629  rexsns  3630  disjsn  3653  snprc  3656  euabsn2  3660  prmg  3712  snssOLD  3717  snssb  3724  difprsnss  3729  eqsnm  3753  snsssn  3759  snsspw  3762  dfnfc2  3825  uni0b  3832  uni0c  3833  sndisj  3996  unidif0  4164  exmid01  4195  rext  4211  exss  4223  frirrg  4346  ordsucim  4495  ordtriexmidlem  4514  ordtri2or2exmidlem  4521  onsucelsucexmidlem  4524  elirr  4536  sucprcreg  4544  fconstmpt  4669  opeliunxp  4677  restidsing  4958  dmsnopg  5095  dfmpt3  5333  nfunsn  5544  fsn  5683  fnasrn  5689  fnasrng  5691  fconstfvm  5729  eusvobj2  5854  opabex3d  6115  opabex3  6116  dcdifsnid  6498  ecexr  6533  ixp0x  6719  xpsnen  6814  fidifsnen  6863  difinfsn  7092  exmidonfinlem  7185  iccid  9899  fzsn  10039  fzpr  10050  fzdifsuc  10054  fsum2dlemstep  11413  prodsnf  11571  fprod1p  11578  fprodunsn  11583  fprod2dlemstep  11601  ef0lem  11639  1nprm  12084  mgmidsssn0  12682  mnd1id  12725  0subm  12748  restsn  13313
  Copyright terms: Public domain W3C validator