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

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

Proof of Theorem sneq
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 eqeq2 2046 . . 3 (A = B → (x = Ax = B))
21abbidv 2152 . 2 (A = B → {xx = A} = {xx = B})
3 df-sn 3373 . 2 {A} = {xx = A}
4 df-sn 3373 . 2 {B} = {xx = B}
52, 3, 43eqtr4g 2094 1 (A = B → {A} = {B})
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242  {cab 2023  {csn 3367
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-sn 3373
This theorem is referenced by:  sneqi  3379  sneqd  3380  euabsn  3431  absneu  3433  preq1  3438  tpeq3  3449  snssg  3491  sneqrg  3524  sneqbg  3525  opeq1  3540  unisng  3588  suceq  4105  snnex  4147  opeliunxp  4338  relop  4429  elimasng  4636  dmsnsnsng  4741  elxp4  4751  elxp5  4752  iotajust  4809  fconstg  5026  f1osng  5110  nfvres  5149  fsng  5279  fnressn  5292  fressnfv  5293  funfvima3  5335  isoselem  5402  1stvalg  5711  2ndvalg  5712  2ndval2  5725  fo1st  5726  fo2nd  5727  f1stres  5728  f2ndres  5729  mpt2mptsx  5765  dmmpt2ssx  5767  fmpt2x  5768  brtpos2  5807  dftpos4  5819  tpostpos  5820  eceq1  6077  ensn1g  6213  en1  6215  xpsneng  6232  xpcomco  6236  xpassen  6240  xpdom2  6241  expival  8891
  Copyright terms: Public domain W3C validator