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 B V
ssexi.2 A B
Assertion ssexi A V

Proof

Step Hyp Ref Expression
1 ssexi.1 B V
2 ssexi.2 A B
3 1 ssex A B A V
4 2 3 ax-mp A V