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

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

Proof of Theorem elsni
StepHypRef Expression
1 elsncg 3389 . 2 (A {B} → (A {B} ↔ A = B))
21ibi 165 1 (A {B} → A = B)
Colors of variables: wff set class
Syntax hints:  wi 4   = 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-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-sn 3373
This theorem is referenced by:  elsnc2g  3396  disjsn2  3424  sssnm  3516  disjxsn  3753  opth1  3964  elsuci  4106  ordtri2orexmid  4211  onsucsssucexmid  4212  sosng  4356  ressn  4801  funcnvsn  4888  fvconst  5294  fmptap  5296  fmptapd  5297  fvunsng  5300  1stconst  5784  2ndconst  5785  reldmtpos  5809  tpostpos  5820  elreal2  6708  ax1rid  6741  ltxrlt  6862  un0addcl  7971  un0mulcl  7972  elfzonlteqm1  8816  1exp  8918  bj-nntrans  9385  bj-nnelirr  9387
  Copyright terms: Public domain W3C validator