Theorem s1eq 14505

Description: Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
s1eq	⊢ (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)

Proof of Theorem s1eq

Step	Hyp	Ref	Expression
1		fveq2 6822	. . . 4 ⊢ (𝐴 = 𝐵 → ( I ‘𝐴) = ( I ‘𝐵))
2	1	opeq2d 4832	. . 3 ⊢ (𝐴 = 𝐵 → ⟨0, ( I ‘𝐴)⟩ = ⟨0, ( I ‘𝐵)⟩)
3	2	sneqd 4588	. 2 ⊢ (𝐴 = 𝐵 → {⟨0, ( I ‘𝐴)⟩} = {⟨0, ( I ‘𝐵)⟩})
4		df-s1 14501	. 2 ⊢ ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
5		df-s1 14501	. 2 ⊢ ⟨“𝐵”⟩ = {⟨0, ( I ‘𝐵)⟩}
6	3, 4, 5	3eqtr4g 2791	1 ⊢ (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)

Syntax hints:   → wi 4   = wceq 1541  {csn 4576  ⟨cop 4582   I cid 5510  ‘cfv 6481  0cc0 11003  ⟨“cs1 14500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-s1 14501

This theorem is referenced by:  s1eqd  14506  wrdl1exs1  14518  wrdl1s1  14519  ccats1pfxeqrex  14619  wrdind  14626  wrd2ind  14627  reuccatpfxs1lem  14650  reuccatpfxs1  14651  revs1  14669  chninf  18538  vrmdval  18762  frgpup3lem  19687  vdegp1ci  29515  clwwlknonwwlknonb  30081  mrsubcv  35542  mrsubrn  35545  elmrsubrn  35552  mrsubvrs  35554  mvhval  35566