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

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

Proof of Theorem s1eqd
StepHypRef Expression
1 s1eqd.1 . 2 (𝜑𝐴 = 𝐵)
2 s1eq 13950 . 2 (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
31, 2syl 17 1 (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  ⟨“cs1 13945
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4550  df-pr 4552  df-op 4556  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351  df-s1 13946
This theorem is referenced by:  s1prc  13954  ccat1st1st  13980  swrds1  14024  swrdlsw  14025  reuccatpfxs1lem  14104  s2eqd  14221  s3eqd  14222  s4eqd  14223  s5eqd  14224  s6eqd  14225  s7eqd  14226  s8eqd  14227  frmdgsum  18023  psgnunilem5  18618  efgredlemc  18867  vrgpval  18889  vrgpinv  18891  frgpup2  18898  frgpup3lem  18899  pfx1s2  30619  pfxlsw2ccat  30630  iwrdsplit  31670  sseqval  31671  sseqf  31675  sseqp1  31678  signsvtn0  31865  signstfveq0  31872  mrsubcv  32782
  Copyright terms: Public domain W3C validator