Theorem s1eqd 14413

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

Step	Hyp	Ref	Expression
1		s1eqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		s1eq 14412	. 2 ⊢ (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)

Syntax hints:   → wi 4   = wceq 1541  ⟨“cs1 14407

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-v 3445  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4278  df-if 4482  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-br 5101  df-iota 6440  df-fv 6496  df-s1 14408

This theorem is referenced by:  s1prc  14416  ccat1st1st  14440  swrds1  14482  swrdlsw  14483  reuccatpfxs1lem  14562  s2eqd  14680  s3eqd  14681  s4eqd  14682  s5eqd  14683  s6eqd  14684  s7eqd  14685  s8eqd  14686  frmdgsum  18602  psgnunilem5  19203  efgredlemc  19451  vrgpval  19473  vrgpinv  19475  frgpup2  19482  frgpup3lem  19483  pfx1s2  31564  pfxlsw2ccat  31575  iwrdsplit  32718  sseqval  32719  sseqf  32723  sseqp1  32726  signsvtn0  32913  signstfveq0  32920  mrsubcv  33835