MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  s1eq Structured version   Visualization version   GIF version

Theorem s1eq 13949
Description: Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
s1eq (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)

Proof of Theorem s1eq
StepHypRef Expression
1 fveq2 6649 . . . 4 (𝐴 = 𝐵 → ( I ‘𝐴) = ( I ‘𝐵))
21opeq2d 4775 . . 3 (𝐴 = 𝐵 → ⟨0, ( I ‘𝐴)⟩ = ⟨0, ( I ‘𝐵)⟩)
32sneqd 4540 . 2 (𝐴 = 𝐵 → {⟨0, ( I ‘𝐴)⟩} = {⟨0, ( I ‘𝐵)⟩})
4 df-s1 13945 . 2 ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
5 df-s1 13945 . 2 ⟨“𝐵”⟩ = {⟨0, ( I ‘𝐵)⟩}
63, 4, 53eqtr4g 2861 1 (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  {csn 4528  cop 4534   I cid 5427  cfv 6328  0cc0 10530  ⟨“cs1 13944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-s1 13945
This theorem is referenced by:  s1eqd  13950  wrdl1exs1  13962  wrdl1s1  13963  ccats1pfxeqrex  14072  wrdind  14079  wrd2ind  14080  reuccatpfxs1lem  14103  reuccatpfxs1  14104  revs1  14122  vrmdval  18018  frgpup3lem  18899  vdegp1ci  27332  clwwlknonwwlknonb  27895  mrsubcv  32871  mrsubrn  32874  elmrsubrn  32881  mrsubvrs  32883  mvhval  32895
  Copyright terms: Public domain W3C validator