Theorem s1eqd 14501

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

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

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 2112  ax-9 2120  ax-ext 2702

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 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-s1 14496

This theorem is referenced by:  s1prc  14504  ccat1st1st  14528  swrds1  14566  swrdlsw  14567  reuccatpfxs1lem  14645  s2eqd  14762  s3eqd  14763  s4eqd  14764  s5eqd  14765  s6eqd  14766  s7eqd  14767  s8eqd  14768  frmdgsum  18762  psgnunilem5  19399  efgredlemc  19650  vrgpval  19672  vrgpinv  19674  frgpup2  19681  frgpup3lem  19682  pfx1s2  32910  pfxlsw2ccat  32921  ccatws1f1olast  32923  wrdpmtrlast  33052  1arithidomlem2  33491  iwrdsplit  34390  sseqval  34391  sseqf  34395  sseqp1  34398  signsvtn0  34573  signstfveq0  34580  mrsubcv  35522