Description: Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | s1eqd.1 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | |
Assertion | s1eqd | ⊢ ( 𝜑 → ⟨“ 𝐴 ”⟩ = ⟨“ 𝐵 ”⟩ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s1eqd.1 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | |
2 | s1eq | ⊢ ( 𝐴 = 𝐵 → ⟨“ 𝐴 ”⟩ = ⟨“ 𝐵 ”⟩ ) | |
3 | 1 2 | syl | ⊢ ( 𝜑 → ⟨“ 𝐴 ”⟩ = ⟨“ 𝐵 ”⟩ ) |