Theorem s1eqd 14306

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

Syntax hints:   → wi 4   = wceq 1539  ⟨“cs1 14300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-s1 14301

This theorem is referenced by:  s1prc  14309  ccat1st1st  14335  swrds1  14379  swrdlsw  14380  reuccatpfxs1lem  14459  s2eqd  14576  s3eqd  14577  s4eqd  14578  s5eqd  14579  s6eqd  14580  s7eqd  14581  s8eqd  14582  frmdgsum  18501  psgnunilem5  19102  efgredlemc  19351  vrgpval  19373  vrgpinv  19375  frgpup2  19382  frgpup3lem  19383  pfx1s2  31213  pfxlsw2ccat  31224  iwrdsplit  32354  sseqval  32355  sseqf  32359  sseqp1  32362  signsvtn0  32549  signstfveq0  32556  mrsubcv  33472