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

Metamath Proof Explorer

Theorem nelcon3d

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

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

Step	Hyp	Ref	Expression
1		nelcon3d.1	$⊢ φ \to (A \in B \to C \in D)$
2	1	con3d	$⊢ φ \to (\neg C \in D \to \neg A \in B)$
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	$⊢ φ \to (C \notin D \to A \notin B)$