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

Theorem sneqd 3435
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 3433 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2syl 14 1 (𝜑 → {𝐴} = {𝐵})
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  {csn 3422
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-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-sn 3428
This theorem is referenced by:  dmsnsnsng  4862  cnvsng  4870  ressn  4925  f1osng  5242  fsng  5412  fnressn  5425  fvsng  5435  2nd1st  5885  dfmpt2  5923  cnvf1olem  5924  tpostpos  5961  tfrlemi1  6029  tfr1onlemaccex  6045  tfrcllemaccex  6058  en1bg  6447  mapsnen  6458  xpassen  6476  fztp  9385  fzsuc2  9386  fseq1p1m1  9401  fseq1m1p1  9402  divalgmod  10707
  Copyright terms: Public domain W3C validator