Theorem s1eqd 14649

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

Syntax hints:   → wi 4   = wceq 1537  ⟨“cs1 14643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-s1 14644

This theorem is referenced by:  s1prc  14652  ccat1st1st  14676  swrds1  14714  swrdlsw  14715  reuccatpfxs1lem  14794  s2eqd  14912  s3eqd  14913  s4eqd  14914  s5eqd  14915  s6eqd  14916  s7eqd  14917  s8eqd  14918  frmdgsum  18897  psgnunilem5  19536  efgredlemc  19787  vrgpval  19809  vrgpinv  19811  frgpup2  19818  frgpup3lem  19819  pfx1s2  32905  pfxlsw2ccat  32917  ccatws1f1olast  32919  wrdpmtrlast  33086  1arithidomlem2  33529  iwrdsplit  34352  sseqval  34353  sseqf  34357  sseqp1  34360  signsvtn0  34547  signstfveq0  34554  mrsubcv  35478