Metamath Proof Explorer

Theorem nelss

Description: Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015)

Ref Expression
Assertion nelss ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) → ¬ 𝐵 ⊆ 𝐶 )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶 ) )
2 1 com12 ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 ⊆ 𝐶 → 𝐴 ∈ 𝐶 ) )
3 2 con3dimp ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) → ¬ 𝐵 ⊆ 𝐶 )