Theorem s1eqd 14526

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

Syntax hints:   → wi 4   = wceq 1540  ⟨“cs1 14520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-s1 14521

This theorem is referenced by:  s1prc  14529  ccat1st1st  14553  swrds1  14591  swrdlsw  14592  reuccatpfxs1lem  14670  s2eqd  14788  s3eqd  14789  s4eqd  14790  s5eqd  14791  s6eqd  14792  s7eqd  14793  s8eqd  14794  frmdgsum  18754  psgnunilem5  19391  efgredlemc  19642  vrgpval  19664  vrgpinv  19666  frgpup2  19673  frgpup3lem  19674  pfx1s2  32893  pfxlsw2ccat  32905  ccatws1f1olast  32907  wrdpmtrlast  33048  1arithidomlem2  33483  iwrdsplit  34354  sseqval  34355  sseqf  34359  sseqp1  34362  signsvtn0  34537  signstfveq0  34544  mrsubcv  35482