Theorem s1eqd 14660

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨“cs1 14654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-s1 14655

This theorem is used by:  s1prc  14663  ccat1st1st  14688  swrds1  14728  swrdlsw  14729  reuccatpfxs1lem  14807  s2eqd  14926  s3eqd  14927  s4eqd  14928  s5eqd  14929  s6eqd  14930  s7eqd  14931  s8eqd  14932  frmdgsum  18952  psgnunilem5  19595  efgredlemc  19846  vrgpval  19868  vrgpinv  19870  frgpup2  19877  frgpup3lem  19878  pfx1s2  33296  pfxlsw2ccat  33303  ccatws1f1olast  33305  wrdpmtrlast  33444  1arithidomlem2  33857  iwrdsplit  34808  sseqval  34809  sseqf  34813  sseqp1  34816  signsvtn0  34988  signstfveq0  34995  mrsubcv  36022