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

Theorem s1eq 13942
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 6663 . . . 4 (𝐴 = 𝐵 → ( I ‘𝐴) = ( I ‘𝐵))
21opeq2d 4802 . . 3 (𝐴 = 𝐵 → ⟨0, ( I ‘𝐴)⟩ = ⟨0, ( I ‘𝐵)⟩)
32sneqd 4569 . 2 (𝐴 = 𝐵 → {⟨0, ( I ‘𝐴)⟩} = {⟨0, ( I ‘𝐵)⟩})
4 df-s1 13938 . 2 ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
5 df-s1 13938 . 2 ⟨“𝐵”⟩ = {⟨0, ( I ‘𝐵)⟩}
63, 4, 53eqtr4g 2878 1 (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  {csn 4557  cop 4563   I cid 5452  cfv 6348  0cc0 10525  ⟨“cs1 13937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-s1 13938
This theorem is referenced by:  s1eqd  13943  wrdl1exs1  13955  wrdl1s1  13956  ccats1pfxeqrex  14065  wrdind  14072  wrd2ind  14073  reuccatpfxs1lem  14096  reuccatpfxs1  14097  revs1  14115  vrmdval  18010  frgpup3lem  18832  vdegp1ci  27247  clwwlknonwwlknonb  27812  mrsubcv  32654  mrsubrn  32657  elmrsubrn  32664  mrsubvrs  32666  mvhval  32678
  Copyright terms: Public domain W3C validator