Theorem ssn0rex

Description: There is an element in a class with a nonempty subclass which is an element of the subclass. (Contributed by AV, 17-Dec-2020)

	Ref	Expression
Assertion	ssn0rex	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssrexv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ) )
2		n0rex	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐴 )
3	1 2	impel	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 )