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 ) |
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 ) |