Metamath Proof Explorer

Theorem caovass

Description: Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 26-May-2014)

Ref Expression
Hypotheses caovass.1 ⊢ A ∈ V
caovass.2 ⊢ B ∈ V
caovass.3 ⊢ C ∈ V
caovass.4 ⊢ x F y F z = x F y F z
Assertion caovass ⊢ A F B F C = A F B F C

Proof

Step Hyp Ref Expression
1 caovass.1 ⊢ A ∈ V
2 caovass.2 ⊢ B ∈ V
3 caovass.3 ⊢ C ∈ V
4 caovass.4 ⊢ x F y F z = x F y F z
5 tru ⊢ ⊤
6 4 a1i ⊢ ⊤ ∧ x ∈ V ∧ y ∈ V ∧ z ∈ V → x F y F z = x F y F z
7 6 caovassg ⊢ ⊤ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A F B F C = A F B F C
8 5 7 mpan ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A F B F C = A F B F C
9 1 2 3 8 mp3an ⊢ A F B F C = A F B F C