This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coeq2

Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997)

Ref Expression
Assertion coeq2 ⊢ A = B → C ∘ A = C ∘ B

Proof

Step Hyp Ref Expression
1 coss2 ⊢ A ⊆ B → C ∘ A ⊆ C ∘ B
2 coss2 ⊢ B ⊆ A → C ∘ B ⊆ C ∘ A
3 1 2 anim12i ⊢ A ⊆ B ∧ B ⊆ A → C ∘ A ⊆ C ∘ B ∧ C ∘ B ⊆ C ∘ A
4 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
5 eqss ⊢ C ∘ A = C ∘ B ↔ C ∘ A ⊆ C ∘ B ∧ C ∘ B ⊆ C ∘ A
6 3 4 5 3imtr4i ⊢ A = B → C ∘ A = C ∘ B