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

Theorem sneq 3602
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 2187 . . 3 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21abbidv 2295 . 2 (𝐴 = 𝐵 → {𝑥𝑥 = 𝐴} = {𝑥𝑥 = 𝐵})
3 df-sn 3597 . 2 {𝐴} = {𝑥𝑥 = 𝐴}
4 df-sn 3597 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
52, 3, 43eqtr4g 2235 1 (𝐴 = 𝐵 → {𝐴} = {𝐵})
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353  {cab 2163  {csn 3591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-sn 3597
This theorem is referenced by:  sneqi  3603  sneqd  3604  euabsn  3661  absneu  3663  preq1  3668  tpeq3  3679  snssgOLD  3727  sneqrg  3760  sneqbg  3761  opeq1  3776  unisng  3824  exmidsssn  4199  exmidsssnc  4200  suceq  4398  snnex  4444  opeliunxp  4677  relop  4772  elimasng  4991  dmsnsnsng  5101  elxp4  5111  elxp5  5112  iotajust  5172  fconstg  5407  f1osng  5497  nfvres  5543  fsng  5684  fnressn  5697  fressnfv  5698  funfvima3  5744  isoselem  5814  1stvalg  6136  2ndvalg  6137  2ndval2  6150  fo1st  6151  fo2nd  6152  f1stres  6153  f2ndres  6154  mpomptsx  6191  dmmpossx  6193  fmpox  6194  brtpos2  6245  dftpos4  6257  tpostpos  6258  eceq1  6563  fvdiagfn  6686  mapsncnv  6688  elixpsn  6728  ixpsnf1o  6729  ensn1g  6790  en1  6792  xpsneng  6815  xpcomco  6819  xpassen  6823  xpdom2  6824  phplem3  6847  phplem3g  6849  fidifsnen  6863  xpfi  6922  pm54.43  7182  cc2lem  7243  cc2  7244  exp3val  10495  fsum2dlemstep  11413  fsumcnv  11416  fisumcom2  11417  fprod2dlemstep  11601  fprodcnv  11604  fprodcom2fi  11605  txswaphmeolem  13453
  Copyright terms: Public domain W3C validator