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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ¬ 𝐴 ⊆ 𝐵 )