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

Theorem elsni 3449
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 3446 . 2 (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
21ibi 174 1 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  wcel 1436  {csn 3431
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-sn 3437
This theorem is referenced by:  elsn2g  3462  disjsn2  3490  sssnm  3583  disjxsn  3820  opth1  4039  elsuci  4206  ordtri2orexmid  4314  onsucsssucexmid  4318  sosng  4481  ressn  4939  funcnvsn  5026  funinsn  5030  fvconst  5450  fmptap  5452  fmptapd  5453  fvunsng  5456  1stconst  5945  2ndconst  5946  reldmtpos  5974  tpostpos  5985  1domsn  6489  ac6sfi  6568  onunsnss  6581  snon0  6598  snexxph  6611  supsnti  6647  djuf1olem  6692  djur  6704  eldju2ndl  6710  eldju2ndr  6711  elreal2  7315  ax1rid  7359  ltxrlt  7499  un0addcl  8642  un0mulcl  8643  elfzonlteqm1  9552  fxnn0nninf  9775  iseqid3  9844  1exp  9886  hashinfuni  10085  hashennnuni  10087  hashprg  10116  zfz1isolemiso  10144  fisumss  10675  sumsnf  10691  divalgmod  10833  phi1  11101  dfphi2  11102  bj-nntrans  11315  bj-nnelirr  11317  exmidsbthrlem  11381
  Copyright terms: Public domain W3C validator