Metamath Proof Explorer

Theorem asslawass

Description: Associativity of an associative operation. (Contributed by FL, 2-Nov-2009) (Revised by AV, 21-Jan-2020)

Ref Expression
Assertion asslawass 
|- ( .o. assLaw M -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )

Proof

Step Hyp Ref Expression
1 df-asslaw 
 |-  assLaw = { <. o , m >. | A. x e. m A. y e. m A. z e. m ( ( x o y ) o z ) = ( x o ( y o z ) ) }
2 1 bropaex12 
 |-  ( .o. assLaw M -> ( .o. e. _V /\ M e. _V ) )
3 isasslaw 
 |-  ( ( .o. e. _V /\ M e. _V ) -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
4 2 3 syl 
 |-  ( .o. assLaw M -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
5 4 ibi 
 |-  ( .o. assLaw M -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )