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

Theorem sneq 3361
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 2031 . . 3 (A = B → (x = Ax = B))
21abbidv 2137 . 2 (A = B → {xx = A} = {xx = B})
3 df-sn 3356 . 2 {A} = {xx = A}
4 df-sn 3356 . 2 {B} = {xx = B}
52, 3, 43eqtr4g 2079 1 (A = B → {A} = {B})
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228  {cab 2008  {csn 3350
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 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-sn 3356
This theorem is referenced by:  sneqi  3362  sneqd  3363  euabsn  3414  absneu  3416  preq1  3421  tpeq3  3432  snssg  3474  sneqrg  3507  sneqbg  3508  opeq1  3523  unisng  3571  suceq  4088  snnex  4131  opeliunxp  4322  relop  4413  elimasng  4620  dmsnsnsng  4725  elxp4  4735  elxp5  4736  iotajust  4793  fconstg  5008  f1osng  5092  nfvres  5131  fsng  5261  fnressn  5274  fressnfv  5275  funfvima3  5317  isoselem  5384  1stvalg  5692  2ndvalg  5693  2ndval2  5706  fo1st  5707  fo2nd  5708  f1stres  5709  f2ndres  5710  mpt2mptsx  5746  dmmpt2ssx  5748  fmpt2x  5749  brtpos2  5788  dftpos4  5800  tpostpos  5801  eceq1  6052
  Copyright terms: Public domain W3C validator