Metamath Proof Explorer


Theorem ssexi

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

Ref Expression
Hypotheses ssexi.1 BV
ssexi.2 AB
Assertion ssexi AV

Proof

Step Hyp Ref Expression
1 ssexi.1 BV
2 ssexi.2 AB
3 1 ssex ABAV
4 2 3 ax-mp AV