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

Theorem sneqd 3415
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 3413 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2syl 14 1 (𝜑 → {𝐴} = {𝐵})
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  {csn 3402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-sn 3408
This theorem is referenced by:  dmsnsnsng  4825  cnvsng  4833  ressn  4885  f1osng  5194  fsng  5363  fnressn  5376  fvsng  5386  2nd1st  5833  dfmpt2  5871  cnvf1olem  5872  tpostpos  5909  tfrlemi1  5976  en1bg  6310  xpassen  6334  fztp  9041  fzsuc2  9042  fseq1p1m1  9057  fseq1m1p1  9058
  Copyright terms: Public domain W3C validator