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

Metamath Proof Explorer

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	$⊢ (A \subseteq B \land A \neq \emptyset) \to \exists x \in B x \in A$

Step	Hyp	Ref	Expression
1		ssrexv	$⊢ A \subseteq B \to (\exists x \in A x \in A \to \exists x \in B x \in A)$
2		n0rex	$⊢ A \neq \emptyset \to \exists x \in A x \in A$
3	1 2	impel	$⊢ (A \subseteq B \land A \neq \emptyset) \to \exists x \in B x \in A$