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 𝐹 = ( 𝑆 × 𝑆 )
	ndmovrcl.3	⊢ ¬ ∅ ∈ 𝑆
Assertion	ndmovrcl	⊢ ( ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		ndmov.1	⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
2		ndmovrcl.3	⊢ ¬ ∅ ∈ 𝑆
3	1	ndmov	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) = ∅ )
4	3	eleq1d	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 ↔ ∅ ∈ 𝑆 ) )
5	2 4	mtbiri	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ¬ ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 )
6	5	con4i	⊢ ( ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )