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	$$⊢\mathrm{dom}F=S\times S$$
	ndmovrcl.3	$$⊢\neg \varnothing \in S$$
Assertion	ndmovrcl	$$⊢AFB\in S\to \left(A\in S\wedge B\in S\right)$$

Proof

Step	Hyp	Ref	Expression
1		ndmov.1	$$⊢\mathrm{dom}F=S\times S$$
2		ndmovrcl.3	$$⊢\neg \varnothing \in S$$
3	1	ndmov	$$⊢\neg \left(A\in S\wedge B\in S\right)\to AFB=\varnothing$$
4	3	eleq1d	$$⊢\neg \left(A\in S\wedge B\in S\right)\to \left(AFB\in S\leftrightarrow \varnothing \in S\right)$$
5	2 4	mtbiri	$$⊢\neg \left(A\in S\wedge B\in S\right)\to \neg AFB\in S$$
6	5	con4i	$$⊢AFB\in S\to \left(A\in S\wedge B\in S\right)$$