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	⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		pssdif	⊢ ( 𝐴 ⊊ 𝐵 → ( 𝐵 ∖ 𝐴 ) ≠ ∅ )
2		n0	⊢ ( ( 𝐵 ∖ 𝐴 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) )
3	1 2	sylib	⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) )
4		eldif	⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) )
5	4	exbii	⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) )
6	3 5	sylib	⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) )