Theorem nssd

Description: Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	nssd.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	nssd.2	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐵 )
Assertion	nssd	⊢ ( 𝜑 → ¬ 𝐴 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nssd.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
2		nssd.2	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐵 )
3	1 2	jca	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐵 ) )
4		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
5		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵 ) )
6	5	notbid	⊢ ( 𝑥 = 𝑋 → ( ¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝑋 ∈ 𝐵 ) )
7	4 6	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐵 ) ) )
8	7	spcegv	⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐵 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ) )
9	1 3 8	sylc	⊢ ( 𝜑 → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
10		nss	⊢ ( ¬ 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
11	9 10	sylibr	⊢ ( 𝜑 → ¬ 𝐴 ⊆ 𝐵 )