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 𝐹 = ( 𝑆 × 𝑆 )
Assertion ndmovcom ( ¬ ( 𝐴𝑆𝐵𝑆 ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐵 𝐹 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ndmov.1 dom 𝐹 = ( 𝑆 × 𝑆 )
2 1 ndmov ( ¬ ( 𝐴𝑆𝐵𝑆 ) → ( 𝐴 𝐹 𝐵 ) = ∅ )
3 ancom ( ( 𝐴𝑆𝐵𝑆 ) ↔ ( 𝐵𝑆𝐴𝑆 ) )
4 1 ndmov ( ¬ ( 𝐵𝑆𝐴𝑆 ) → ( 𝐵 𝐹 𝐴 ) = ∅ )
5 3 4 sylnbi ( ¬ ( 𝐴𝑆𝐵𝑆 ) → ( 𝐵 𝐹 𝐴 ) = ∅ )
6 2 5 eqtr4d ( ¬ ( 𝐴𝑆𝐵𝑆 ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐵 𝐹 𝐴 ) )