Theorem nelcon3d

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

	Ref	Expression
Hypothesis	nelcon3d.1	⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷 ) )
Assertion	nelcon3d	⊢ ( 𝜑 → ( 𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nelcon3d.1	⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷 ) )
2	1	con3d	⊢ ( 𝜑 → ( ¬ 𝐶 ∈ 𝐷 → ¬ 𝐴 ∈ 𝐵 ) )
3		df-nel	⊢ ( 𝐶 ∉ 𝐷 ↔ ¬ 𝐶 ∈ 𝐷 )
4		df-nel	⊢ ( 𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵 )
5	2 3 4	3imtr4g	⊢ ( 𝜑 → ( 𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵 ) )