Theorem s1eqd 14566

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

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

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-s1 14561

This theorem is referenced by:  s1prc  14569  ccat1st1st  14593  swrds1  14631  swrdlsw  14632  reuccatpfxs1lem  14711  s2eqd  14829  s3eqd  14830  s4eqd  14831  s5eqd  14832  s6eqd  14833  s7eqd  14834  s8eqd  14835  frmdgsum  18789  psgnunilem5  19424  efgredlemc  19675  vrgpval  19697  vrgpinv  19699  frgpup2  19706  frgpup3lem  19707  pfx1s2  32860  pfxlsw2ccat  32872  ccatws1f1olast  32874  wrdpmtrlast  33050  1arithidomlem2  33507  iwrdsplit  34378  sseqval  34379  sseqf  34383  sseqp1  34386  signsvtn0  34561  signstfveq0  34568  mrsubcv  35497