Theorem s1eqd 13946

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

Syntax hints:   → wi 4   = wceq 1538  ⟨“cs1 13940

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-s1 13941

This theorem is referenced by:  s1prc  13949  ccat1st1st  13975  swrds1  14019  swrdlsw  14020  reuccatpfxs1lem  14099  s2eqd  14216  s3eqd  14217  s4eqd  14218  s5eqd  14219  s6eqd  14220  s7eqd  14221  s8eqd  14222  frmdgsum  18019  psgnunilem5  18614  efgredlemc  18863  vrgpval  18885  vrgpinv  18887  frgpup2  18894  frgpup3lem  18895  pfx1s2  30641  pfxlsw2ccat  30652  iwrdsplit  31755  sseqval  31756  sseqf  31760  sseqp1  31763  signsvtn0  31950  signstfveq0  31957  mrsubcv  32870