Description: Any operation is commutative outside its domain. (Contributed by NM, 24-Aug-1995)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ndmov.1 | |- dom F = ( S X. S ) |
|
Assertion | ndmovcom | |- ( -. ( A e. S /\ B e. S ) -> ( A F B ) = ( B F A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ndmov.1 | |- dom F = ( S X. S ) |
|
2 | 1 | ndmov | |- ( -. ( A e. S /\ B e. S ) -> ( A F B ) = (/) ) |
3 | ancom | |- ( ( A e. S /\ B e. S ) <-> ( B e. S /\ A e. S ) ) |
|
4 | 1 | ndmov | |- ( -. ( B e. S /\ A e. S ) -> ( B F A ) = (/) ) |
5 | 3 4 | sylnbi | |- ( -. ( A e. S /\ B e. S ) -> ( B F A ) = (/) ) |
6 | 2 5 | eqtr4d | |- ( -. ( A e. S /\ B e. S ) -> ( A F B ) = ( B F A ) ) |