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

Theorem elsni 3609
Description: There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
elsni (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Proof of Theorem elsni
StepHypRef Expression
1 elsng 3606 . 2 (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
21ibi 176 1 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353  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:  elsn2g  3624  nelsn  3626  disjsn2  3654  sssnm  3752  disjxsn  3998  pwntru  4196  opth1  4232  elsuci  4399  ordtri2orexmid  4518  onsucsssucexmid  4522  sosng  4695  elrelimasn  4989  ressn  5164  funcnvsn  5256  funinsn  5260  fvconst  5699  fmptap  5701  fmptapd  5702  fvunsng  5705  mposnif  5962  1stconst  6215  2ndconst  6216  reldmtpos  6247  tpostpos  6258  1domsn  6812  ac6sfi  6891  onunsnss  6909  snon0  6928  snexxph  6942  elfi2  6964  supsnti  6997  djuf1olem  7045  eldju2ndl  7064  eldju2ndr  7065  difinfsnlem  7091  pw1on  7218  elreal2  7807  ax1rid  7854  ltxrlt  8000  un0addcl  9185  un0mulcl  9186  elfzonlteqm1  10183  fxnn0nninf  10411  1exp  10522  hashinfuni  10728  hashennnuni  10730  hashprg  10759  zfz1isolemiso  10790  fisumss  11371  sumsnf  11388  fsumsplitsn  11389  fsum2dlemstep  11413  fisumcom2  11417  fprodssdc  11569  fprodunsn  11583  fprod2dlemstep  11601  fprodcom2fi  11605  fprodsplitsn  11612  divalgmod  11902  phi1  12189  dfphi2  12190  nnnn0modprm0  12225  exmidunben  12397  txdis1cn  13411  bj-nntrans  14325  bj-nnelirr  14327  pwtrufal  14369  sssneq  14374  exmidsbthrlem  14393
  Copyright terms: Public domain W3C validator