Theorem s1eqd 14564

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

Syntax hints:   → wi 4   = wceq 1542  ⟨“cs1 14558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-s1 14559

This theorem is referenced by:  s1prc  14567  ccat1st1st  14591  swrds1  14629  swrdlsw  14630  reuccatpfxs1lem  14708  s2eqd  14825  s3eqd  14826  s4eqd  14827  s5eqd  14828  s6eqd  14829  s7eqd  14830  s8eqd  14831  frmdgsum  18830  psgnunilem5  19469  efgredlemc  19720  vrgpval  19742  vrgpinv  19744  frgpup2  19751  frgpup3lem  19752  pfx1s2  32999  pfxlsw2ccat  33010  ccatws1f1olast  33012  wrdpmtrlast  33154  1arithidomlem2  33596  iwrdsplit  34531  sseqval  34532  sseqf  34536  sseqp1  34539  signsvtn0  34714  signstfveq0  34721  mrsubcv  35692