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

Theorem sneq 3414
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 2065 . . 3  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21abbidv 2171 . 2  |-  ( A  =  B  ->  { x  |  x  =  A }  =  { x  |  x  =  B } )
3 df-sn 3409 . 2  |-  { A }  =  { x  |  x  =  A }
4 df-sn 3409 . 2  |-  { B }  =  { x  |  x  =  B }
52, 3, 43eqtr4g 2113 1  |-  ( A  =  B  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259   {cab 2042   {csn 3403
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 3409
This theorem is referenced by:  sneqi  3415  sneqd  3416  euabsn  3468  absneu  3470  preq1  3475  tpeq3  3486  snssg  3528  sneqrg  3561  sneqbg  3562  opeq1  3577  unisng  3625  suceq  4167  snnex  4209  opeliunxp  4423  relop  4514  elimasng  4721  dmsnsnsng  4826  elxp4  4836  elxp5  4837  iotajust  4894  fconstg  5111  f1osng  5195  nfvres  5234  fsng  5364  fnressn  5377  fressnfv  5378  funfvima3  5420  isoselem  5487  1stvalg  5797  2ndvalg  5798  2ndval2  5811  fo1st  5812  fo2nd  5813  f1stres  5814  f2ndres  5815  mpt2mptsx  5851  dmmpt2ssx  5853  fmpt2x  5854  brtpos2  5897  dftpos4  5909  tpostpos  5910  eceq1  6172  ensn1g  6308  en1  6310  xpsneng  6327  xpcomco  6331  xpassen  6335  xpdom2  6336  phplem3  6348  phplem3g  6350  fidifsnen  6362  expival  9422
  Copyright terms: Public domain W3C validator