**Description:** Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004)

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

Hypotheses | sseqtrd.1 | $${\u22a2}{\phi}\to {A}\subseteq {B}$$ | |

sseqtrd.2 | $${\u22a2}{\phi}\to {B}={C}$$ | ||

Assertion | sseqtrd | $${\u22a2}{\phi}\to {A}\subseteq {C}$$ |

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

1 | sseqtrd.1 | $${\u22a2}{\phi}\to {A}\subseteq {B}$$ | |

2 | sseqtrd.2 | $${\u22a2}{\phi}\to {B}={C}$$ | |

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

4 | 1 3 | mpbid | $${\u22a2}{\phi}\to {A}\subseteq {C}$$ |