Theorem nelcon3d

Description: Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020)

	Ref	Expression
Hypothesis	nelcon3d.1	$$⊢\phi \to \left(A\in B\to C\in D\right)$$
Assertion	nelcon3d	$$⊢\phi \to \left(C\notin D\to A\notin B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nelcon3d.1	$$⊢\phi \to \left(A\in B\to C\in D\right)$$
2	1	con3d	$$⊢\phi \to \left(\neg C\in D\to \neg A\in B\right)$$
3		df-nel	$$⊢C\notin D\leftrightarrow \neg C\in D$$
4		df-nel	$$⊢A\notin B\leftrightarrow \neg A\in B$$
5	2 3 4	3imtr4g	$$⊢\phi \to \left(C\notin D\to A\notin B\right)$$