Theorem s1eqd 14562

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

Syntax hints:   → wi 4   = wceq 1547  ⟨“cs1 14556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-s1 14557

This theorem is referenced by:  s1prc  14565  ccat1st1st  14589  swrds1  14627  swrdlsw  14628  reuccatpfxs1lem  14706  s2eqd  14823  s3eqd  14824  s4eqd  14825  s5eqd  14826  s6eqd  14827  s7eqd  14828  s8eqd  14829  frmdgsum  18828  psgnunilem5  19467  efgredlemc  19718  vrgpval  19740  vrgpinv  19742  frgpup2  19749  frgpup3lem  19750  pfx1s2  33025  pfxlsw2ccat  33036  ccatws1f1olast  33038  wrdpmtrlast  33181  1arithidomlem2  33626  iwrdsplit  34578  sseqval  34579  sseqf  34583  sseqp1  34586  signsvtn0  34761  signstfveq0  34768  mrsubcv  35745