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

Theorem sneq 3383
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 2049 . . 3  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21abbidv 2155 . 2  |-  ( A  =  B  ->  { x  |  x  =  A }  =  { x  |  x  =  B } )
3 df-sn 3378 . 2  |-  { A }  =  { x  |  x  =  A }
4 df-sn 3378 . 2  |-  { B }  =  { x  |  x  =  B }
52, 3, 43eqtr4g 2097 1  |-  ( A  =  B  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243   {cab 2026   {csn 3372
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 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-sn 3378
This theorem is referenced by:  sneqi  3384  sneqd  3385  euabsn  3437  absneu  3439  preq1  3444  tpeq3  3455  snssg  3497  sneqrg  3530  sneqbg  3531  opeq1  3546  unisng  3594  suceq  4135  snnex  4177  opeliunxp  4382  relop  4473  elimasng  4680  dmsnsnsng  4785  elxp4  4795  elxp5  4796  iotajust  4853  fconstg  5070  f1osng  5154  nfvres  5193  fsng  5323  fnressn  5336  fressnfv  5337  funfvima3  5379  isoselem  5446  1stvalg  5756  2ndvalg  5757  2ndval2  5770  fo1st  5771  fo2nd  5772  f1stres  5773  f2ndres  5774  mpt2mptsx  5810  dmmpt2ssx  5812  fmpt2x  5813  brtpos2  5853  dftpos4  5865  tpostpos  5866  eceq1  6128  ensn1g  6264  en1  6266  xpsneng  6283  xpcomco  6287  xpassen  6291  xpdom2  6292  phplem3  6304  phplem3g  6306  fidifsnen  6318  expival  9135
  Copyright terms: Public domain W3C validator