**Description:** An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994)

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

Hypothesis | sseq1d.1 | $${\u22a2}{\phi}\to {A}={B}$$ | |

Assertion | sseq2d | $${\u22a2}{\phi}\to \left({C}\subseteq {A}\leftrightarrow {C}\subseteq {B}\right)$$ |

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

1 | sseq1d.1 | $${\u22a2}{\phi}\to {A}={B}$$ | |

2 | sseq2 | $${\u22a2}{A}={B}\to \left({C}\subseteq {A}\leftrightarrow {C}\subseteq {B}\right)$$ | |

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