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

Metamath Proof Explorer

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 × S
ndmovrcl.3 ⊢ ¬ ∅ ∈ S
Assertion ndmovrcl ⊢ A F B ∈ S → A ∈ S ∧ B ∈ S

Proof

Step Hyp Ref Expression
1 ndmov.1 ⊢ dom ⁡ F = S × S
2 ndmovrcl.3 ⊢ ¬ ∅ ∈ S
3 1 ndmov ⊢ ¬ A ∈ S ∧ B ∈ S → A F B = ∅
4 3 eleq1d ⊢ ¬ A ∈ S ∧ B ∈ S → A F B ∈ S ↔ ∅ ∈ S
5 2 4 mtbiri ⊢ ¬ A ∈ S ∧ B ∈ S → ¬ A F B ∈ S
6 5 con4i ⊢ A F B ∈ S → A ∈ S ∧ B ∈ S