Theorem ssexnelpss

Description: If there is an element of a class which is not contained in a subclass, the subclass is a proper subclass. (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Assertion	ssexnelpss	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝑥 ∉ 𝐴 ) → 𝐴 ⊊ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-nel	⊢ ( 𝑥 ∉ 𝐴 ↔ ¬ 𝑥 ∈ 𝐴 )
2		ssnelpss	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝐴 ⊊ 𝐵 ) )
3	2	expdimp	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ 𝐴 → 𝐴 ⊊ 𝐵 ) )
4	1 3	biimtrid	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∉ 𝐴 → 𝐴 ⊊ 𝐵 ) )
5	4	rexlimdva	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑥 ∈ 𝐵 𝑥 ∉ 𝐴 → 𝐴 ⊊ 𝐵 ) )
6	5	imp	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝑥 ∉ 𝐴 ) → 𝐴 ⊊ 𝐵 )