Metamath Proof Explorer

Theorem ssex

Description: The subset of a set is also a set. Exercise 3 of TakeutiZaring p. 22. This is one way to express the Axiom of Separation ax-sep (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994)

Ref Expression
Hypothesis ssex.1 B V
Assertion ssex A B A V


Step Hyp Ref Expression
1 ssex.1 B V
2 df-ss A B A B = A
3 1 inex2 A B V
4 eleq1 A B = A A B V A V
5 3 4 mpbii A B = A A V
6 2 5 sylbi A B A V