**Description:** The singleton of an element of a class is a subset of the class
(deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

Ref | Expression | ||
---|---|---|---|

Hypothesis | snssd.1 | $${\u22a2}{\phi}\to {A}\in {B}$$ | |

Assertion | snssd | $${\u22a2}{\phi}\to \left\{{A}\right\}\subseteq {B}$$ |

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

1 | snssd.1 | $${\u22a2}{\phi}\to {A}\in {B}$$ | |

2 | snssi | $${\u22a2}{A}\in {B}\to \left\{{A}\right\}\subseteq {B}$$ | |

3 | 1 2 | syl | $${\u22a2}{\phi}\to \left\{{A}\right\}\subseteq {B}$$ |