This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \times S$
	Assertion	ndmovcom	$⊢ \neg (A \in S \land B \in S) \to A F B = B F A$

Step	Hyp	Ref	Expression
1		ndmov.1	$⊢ dom F = S \times S$
2	1	ndmov	$⊢ \neg (A \in S \land B \in S) \to A F B = \emptyset$
3		ancom	$⊢ (A \in S \land B \in S) \leftrightarrow (B \in S \land A \in S)$
4	1	ndmov	$⊢ \neg (B \in S \land A \in S) \to B F A = \emptyset$
5	3 4	sylnbi	$⊢ \neg (A \in S \land B \in S) \to B F A = \emptyset$
6	2 5	eqtr4d	$⊢ \neg (A \in S \land B \in S) \to A F B = B F A$