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

Theorem sneq 3413
Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sneq (𝐴 = 𝐵 → {𝐴} = {𝐵})

Proof of Theorem sneq
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqeq2 2065 . . 3 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21abbidv 2171 . 2 (𝐴 = 𝐵 → {𝑥𝑥 = 𝐴} = {𝑥𝑥 = 𝐵})
3 df-sn 3408 . 2 {𝐴} = {𝑥𝑥 = 𝐴}
4 df-sn 3408 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
52, 3, 43eqtr4g 2113 1 (𝐴 = 𝐵 → {𝐴} = {𝐵})
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  {cab 2042  {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:  sneqi  3414  sneqd  3415  euabsn  3467  absneu  3469  preq1  3474  tpeq3  3485  snssg  3527  sneqrg  3560  sneqbg  3561  opeq1  3576  unisng  3624  suceq  4166  snnex  4208  opeliunxp  4422  relop  4513  elimasng  4720  dmsnsnsng  4825  elxp4  4835  elxp5  4836  iotajust  4893  fconstg  5110  f1osng  5194  nfvres  5233  fsng  5363  fnressn  5376  fressnfv  5377  funfvima3  5419  isoselem  5486  1stvalg  5796  2ndvalg  5797  2ndval2  5810  fo1st  5811  fo2nd  5812  f1stres  5813  f2ndres  5814  mpt2mptsx  5850  dmmpt2ssx  5852  fmpt2x  5853  brtpos2  5896  dftpos4  5908  tpostpos  5909  eceq1  6171  ensn1g  6307  en1  6309  xpsneng  6326  xpcomco  6330  xpassen  6334  xpdom2  6335  phplem3  6347  phplem3g  6349  fidifsnen  6361  expival  9416
  Copyright terms: Public domain W3C validator