Theorem s1eqd 14636

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

Syntax hints:   → wi 4   = wceq 1537  ⟨“cs1 14630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-s1 14631

This theorem is referenced by:  s1prc  14639  ccat1st1st  14663  swrds1  14701  swrdlsw  14702  reuccatpfxs1lem  14781  s2eqd  14899  s3eqd  14900  s4eqd  14901  s5eqd  14902  s6eqd  14903  s7eqd  14904  s8eqd  14905  frmdgsum  18888  psgnunilem5  19527  efgredlemc  19778  vrgpval  19800  vrgpinv  19802  frgpup2  19809  frgpup3lem  19810  pfx1s2  32908  pfxlsw2ccat  32920  ccatws1f1olast  32922  wrdpmtrlast  33096  1arithidomlem2  33544  iwrdsplit  34369  sseqval  34370  sseqf  34374  sseqp1  34377  signsvtn0  34564  signstfveq0  34571  mrsubcv  35495