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

Ref | Expression | ||
---|---|---|---|

Assertion | s1eq | ⊢ ( 𝐴 = 𝐵 → ⟨“ 𝐴 ”⟩ = ⟨“ 𝐵 ”⟩ ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | fveq2 | ⊢ ( 𝐴 = 𝐵 → ( I ‘ 𝐴 ) = ( I ‘ 𝐵 ) ) | |

2 | 1 | opeq2d | ⊢ ( 𝐴 = 𝐵 → ⟨ 0 , ( I ‘ 𝐴 ) ⟩ = ⟨ 0 , ( I ‘ 𝐵 ) ⟩ ) |

3 | 2 | sneqd | ⊢ ( 𝐴 = 𝐵 → { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ } = { ⟨ 0 , ( I ‘ 𝐵 ) ⟩ } ) |

4 | df-s1 | ⊢ ⟨“ 𝐴 ”⟩ = { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ } | |

5 | df-s1 | ⊢ ⟨“ 𝐵 ”⟩ = { ⟨ 0 , ( I ‘ 𝐵 ) ⟩ } | |

6 | 3 4 5 | 3eqtr4g | ⊢ ( 𝐴 = 𝐵 → ⟨“ 𝐴 ”⟩ = ⟨“ 𝐵 ”⟩ ) |