Theorem ssexi

Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993)

	Ref	Expression
Hypotheses	ssexi.1	|- B e. _V
	ssexi.2	|- A C_ B
Assertion	ssexi	|- A e. _V

Proof

Step	Hyp	Ref	Expression
1		ssexi.1	|- B e. _V
2		ssexi.2	|- A C_ B
3	1	ssex	|- ( A C_ B -> A e. _V )
4	2 3	ax-mp	|- A e. _V