Theorem s1eqd 14775

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-s1 14770

This theorem is used by:  s1prc  14778  ccat1st1st  14804  swrds1  14844  swrdlsw  14845  reuccatpfxs1lem  14923  s2eqd  15042  s3eqd  15043  s4eqd  15044  s5eqd  15045  s6eqd  15046  s7eqd  15047  s8eqd  15048  frmdgsum  19087  psgnunilem5  19738  efgredlemc  19989  vrgpval  20011  vrgpinv  20013  frgpup2  20020  frgpup3lem  20021  pfx1s2  33576  pfxlsw2ccat  33583  ccatws1f1olast  33585  wrdpmtrlast  33724  1arithidomlem2  34138  iwrdsplit  35089  sseqval  35090  sseqf  35094  sseqp1  35097  signsvtn0  35269  signstfveq0  35276  mrsubcv  36442