Theorem s1eqd 14604

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

Syntax hints:   → wi 4   = wceq 1533  ⟨“cs1 14598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-iota 6505  df-fv 6561  df-s1 14599

This theorem is referenced by:  s1prc  14607  ccat1st1st  14631  swrds1  14669  swrdlsw  14670  reuccatpfxs1lem  14749  s2eqd  14867  s3eqd  14868  s4eqd  14869  s5eqd  14870  s6eqd  14871  s7eqd  14872  s8eqd  14873  frmdgsum  18847  psgnunilem5  19487  efgredlemc  19738  vrgpval  19760  vrgpinv  19762  frgpup2  19769  frgpup3lem  19770  pfx1s2  32791  pfxlsw2ccat  32802  ccatws1f1olast  32804  wrdpmtrlast  32948  1arithidomlem2  33388  iwrdsplit  34177  sseqval  34178  sseqf  34182  sseqp1  34185  signsvtn0  34372  signstfveq0  34379  mrsubcv  35290