Theorem s1eqd 14519

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 14518	. 2 ⊢ (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-s1 14514

This theorem is referenced by:  s1prc  14522  ccat1st1st  14546  swrds1  14584  swrdlsw  14585  reuccatpfxs1lem  14663  s2eqd  14780  s3eqd  14781  s4eqd  14782  s5eqd  14783  s6eqd  14784  s7eqd  14785  s8eqd  14786  frmdgsum  18780  psgnunilem5  19416  efgredlemc  19667  vrgpval  19689  vrgpinv  19691  frgpup2  19698  frgpup3lem  19699  pfx1s2  32931  pfxlsw2ccat  32942  ccatws1f1olast  32944  wrdpmtrlast  33073  1arithidomlem2  33512  iwrdsplit  34411  sseqval  34412  sseqf  34416  sseqp1  34419  signsvtn0  34594  signstfveq0  34601  mrsubcv  35565