**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 | $${\u22a2}{B}\in \mathrm{V}$$ | |

Assertion | ssex | $${\u22a2}{A}\subseteq {B}\to {A}\in \mathrm{V}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | ssex.1 | $${\u22a2}{B}\in \mathrm{V}$$ | |

2 | df-ss | $${\u22a2}{A}\subseteq {B}\leftrightarrow {A}\cap {B}={A}$$ | |

3 | 1 | inex2 | $${\u22a2}{A}\cap {B}\in \mathrm{V}$$ |

4 | eleq1 | $${\u22a2}{A}\cap {B}={A}\to \left({A}\cap {B}\in \mathrm{V}\leftrightarrow {A}\in \mathrm{V}\right)$$ | |

5 | 3 4 | mpbii | $${\u22a2}{A}\cap {B}={A}\to {A}\in \mathrm{V}$$ |

6 | 2 5 | sylbi | $${\u22a2}{A}\subseteq {B}\to {A}\in \mathrm{V}$$ |