Theorem s1eqd 14612

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

Syntax hints:   → wi 4   = wceq 1559  ⟨“cs1 14606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-s1 14607

This theorem is referenced by:  s1prc  14615  ccat1st1st  14639  swrds1  14677  swrdlsw  14678  reuccatpfxs1lem  14756  s2eqd  14873  s3eqd  14874  s4eqd  14875  s5eqd  14876  s6eqd  14877  s7eqd  14878  s8eqd  14879  frmdgsum  18879  psgnunilem5  19517  efgredlemc  19768  vrgpval  19790  vrgpinv  19792  frgpup2  19799  frgpup3lem  19800  pfx1s2  33078  pfxlsw2ccat  33089  ccatws1f1olast  33091  wrdpmtrlast  33234  1arithidomlem2  33693  iwrdsplit  34645  sseqval  34646  sseqf  34650  sseqp1  34653  signsvtn0  34828  signstfveq0  34835  mrsubcv  35824