Metamath Proof Explorer


Theorem caovcom

Description: Convert an operation commutative law to class notation. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 1-Jun-2013)

Ref Expression
Hypotheses caovcom.1
|- A e. _V
caovcom.2
|- B e. _V
caovcom.3
|- ( x F y ) = ( y F x )
Assertion caovcom
|- ( A F B ) = ( B F A )

Proof

Step Hyp Ref Expression
1 caovcom.1
 |-  A e. _V
2 caovcom.2
 |-  B e. _V
3 caovcom.3
 |-  ( x F y ) = ( y F x )
4 1 2 pm3.2i
 |-  ( A e. _V /\ B e. _V )
5 3 a1i
 |-  ( ( A e. _V /\ ( x e. _V /\ y e. _V ) ) -> ( x F y ) = ( y F x ) )
6 5 caovcomg
 |-  ( ( A e. _V /\ ( A e. _V /\ B e. _V ) ) -> ( A F B ) = ( B F A ) )
7 1 4 6 mp2an
 |-  ( A F B ) = ( B F A )