Description: The commutes relation is reflexive. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cmid.1 | ⊢ 𝐴 ∈ Cℋ | |
Assertion | cmidi | ⊢ 𝐴 𝐶ℋ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmid.1 | ⊢ 𝐴 ∈ Cℋ | |
2 | ssid | ⊢ 𝐴 ⊆ 𝐴 | |
3 | 1 1 2 | lecmii | ⊢ 𝐴 𝐶ℋ 𝐴 |