**Description:** An element of a power class is a subclass. Deduction form of elpwi .
(Contributed by David Moews, 1-May-2017)

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

Hypothesis | elpwid.1 | $${\u22a2}{\phi}\to {A}\in \mathcal{P}{B}$$ | |

Assertion | elpwid | $${\u22a2}{\phi}\to {A}\subseteq {B}$$ |

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

1 | elpwid.1 | $${\u22a2}{\phi}\to {A}\in \mathcal{P}{B}$$ | |

2 | elpwi | $${\u22a2}{A}\in \mathcal{P}{B}\to {A}\subseteq {B}$$ | |

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