Metamath Proof Explorer


Theorem ndmovcom

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

Proof

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