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

Theorem sneqd 3546
 Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)
Hypothesis
Ref Expression
sneqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
sneqd (𝜑 → {𝐴} = {𝐵})

Proof of Theorem sneqd
StepHypRef Expression
1 sneqd.1 . 2 (𝜑𝐴 = 𝐵)
2 sneq 3544 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2syl 14 1 (𝜑 → {𝐴} = {𝐵})
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332  {csn 3533 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-sn 3539 This theorem is referenced by:  dmsnsnsng  5025  cnvsng  5033  ressn  5088  f1osng  5417  fsng  5602  fnressn  5615  fvsng  5625  2nd1st  6087  dfmpo  6129  cnvf1olem  6130  tpostpos  6170  tfrlemi1  6238  tfr1onlemaccex  6254  tfrcllemaccex  6267  elixpsn  6638  ixpsnf1o  6639  en1bg  6703  mapsnen  6714  xpassen  6733  fztp  9909  fzsuc2  9910  fseq1p1m1  9925  fseq1m1p1  9926  zfz1isolemsplit  10633  zfz1isolem1  10635  fsumm1  11237  divalgmod  11680  ennnfonelemg  11972  ennnfonelemp1  11975  ennnfonelem1  11976  ennnfonelemnn0  11991  setsvalg  12048  strsetsid  12051  txdis  12505
 Copyright terms: Public domain W3C validator