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

Metamath Proof Explorer

Theorem pssnel

Description: A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996)

Ref Expression
Assertion pssnel ⊢ A ⊂ B → ∃ x x ∈ B ∧ ¬ x ∈ A

Proof

Step Hyp Ref Expression
1 pssdif ⊢ A ⊂ B → B ∖ A ≠ ∅
2 n0 ⊢ B ∖ A ≠ ∅ ↔ ∃ x x ∈ B ∖ A
3 1 2 sylib ⊢ A ⊂ B → ∃ x x ∈ B ∖ A
4 eldif ⊢ x ∈ B ∖ A ↔ x ∈ B ∧ ¬ x ∈ A
5 4 exbii ⊢ ∃ x x ∈ B ∖ A ↔ ∃ x x ∈ B ∧ ¬ x ∈ A
6 3 5 sylib ⊢ A ⊂ B → ∃ x x ∈ B ∧ ¬ x ∈ A