Theorem s1eqd 13691

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

Syntax hints:   → wi 4   = wceq 1601  ⟨“cs1 13685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-s1 13686

This theorem is referenced by:  s1prc  13694  ccat1st1st  13718  swrds1  13771  swrdlsw  13772  swrdccatwrdOLD  13830  reuccatpfxs1lem  13882  s2eqd  14014  s3eqd  14015  s4eqd  14016  s5eqd  14017  s6eqd  14018  s7eqd  14019  s8eqd  14020  frmdgsum  17786  psgnunilem5  18297  psgnunilem5OLD  18298  efgredlemc  18543  vrgpval  18566  vrgpinv  18568  frgpup2  18575  frgpup3lem  18576  iwrdsplit  31047  iwrdsplitOLD  31048  sseqval  31049  sseqf  31053  sseqp1  31056  signsvtn0  31247  signsvtn0OLD  31248  signstfveq0  31255  signstfveq0OLD  31256  mrsubcv  32006