Theorem s1eqd 14547

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

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

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 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-s1 14542

This theorem is referenced by:  s1prc  14550  ccat1st1st  14574  swrds1  14612  swrdlsw  14613  reuccatpfxs1lem  14692  s2eqd  14810  s3eqd  14811  s4eqd  14812  s5eqd  14813  s6eqd  14814  s7eqd  14815  s8eqd  14816  frmdgsum  18739  psgnunilem5  19356  efgredlemc  19607  vrgpval  19629  vrgpinv  19631  frgpup2  19638  frgpup3lem  19639  pfx1s2  32092  pfxlsw2ccat  32103  iwrdsplit  33374  sseqval  33375  sseqf  33379  sseqp1  33382  signsvtn0  33569  signstfveq0  33576  mrsubcv  34489