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

Metamath Proof Explorer

Theorem caovassg

Description: Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013) (Revised by Mario Carneiro, 26-May-2014)

Ref Expression
Hypothesis caovassg.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S → x F y F z = x F y F z
Assertion caovassg ⊢ φ ∧ A ∈ S ∧ B ∈ S ∧ C ∈ S → A F B F C = A F B F C

Proof

Step Hyp Ref Expression
1 caovassg.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S → x F y F z = x F y F z
2 1 ralrimivvva ⊢ φ → ∀ x ∈ S ∀ y ∈ S ∀ z ∈ S x F y F z = x F y F z
3 oveq1 ⊢ x = A → x F y = A F y
4 3 oveq1d ⊢ x = A → x F y F z = A F y F z
5 oveq1 ⊢ x = A → x F y F z = A F y F z
6 4 5 eqeq12d ⊢ x = A → x F y F z = x F y F z ↔ A F y F z = A F y F z
7 oveq2 ⊢ y = B → A F y = A F B
8 7 oveq1d ⊢ y = B → A F y F z = A F B F z
9 oveq1 ⊢ y = B → y F z = B F z
10 9 oveq2d ⊢ y = B → A F y F z = A F B F z
11 8 10 eqeq12d ⊢ y = B → A F y F z = A F y F z ↔ A F B F z = A F B F z
12 oveq2 ⊢ z = C → A F B F z = A F B F C
13 oveq2 ⊢ z = C → B F z = B F C
14 13 oveq2d ⊢ z = C → A F B F z = A F B F C
15 12 14 eqeq12d ⊢ z = C → A F B F z = A F B F z ↔ A F B F C = A F B F C
16 6 11 15 rspc3v ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ S → ∀ x ∈ S ∀ y ∈ S ∀ z ∈ S x F y F z = x F y F z → A F B F C = A F B F C
17 2 16 mpan9 ⊢ φ ∧ A ∈ S ∧ B ∈ S ∧ C ∈ S → A F B F C = A F B F C