Theorem ndmovrcl

Description: Reverse closure law, when an operation's domain doesn't contain the empty set. (Contributed by NM, 3-Feb-1996)

	Ref	Expression
Hypotheses	ndmov.1	|- dom F = ( S X. S )
	ndmovrcl.3	|- -. (/) e. S
Assertion	ndmovrcl	|- ( ( A F B ) e. S -> ( A e. S /\ B e. S ) )

Proof

Step	Hyp	Ref	Expression
1		ndmov.1	|- dom F = ( S X. S )
2		ndmovrcl.3	|- -. (/) e. S
3	1	ndmov	|- ( -. ( A e. S /\ B e. S ) -> ( A F B ) = (/) )
4	3	eleq1d	|- ( -. ( A e. S /\ B e. S ) -> ( ( A F B ) e. S <-> (/) e. S ) )
5	2 4	mtbiri	|- ( -. ( A e. S /\ B e. S ) -> -. ( A F B ) e. S )
6	5	con4i	|- ( ( A F B ) e. S -> ( A e. S /\ B e. S ) )