**Description:** Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998)

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

Assertion | sseq2 | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵 ) ) |

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

1 | sstr2 | ⊢ ( 𝐶 ⊆ 𝐴 → ( 𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵 ) ) | |

2 | 1 | com12 | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵 ) ) |

3 | sstr2 | ⊢ ( 𝐶 ⊆ 𝐵 → ( 𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴 ) ) | |

4 | 3 | com12 | ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴 ) ) |

5 | 2 4 | anim12i | ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵 ) ∧ ( 𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴 ) ) ) |

6 | eqss | ⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ) | |

7 | dfbi2 | ⊢ ( ( 𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵 ) ↔ ( ( 𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵 ) ∧ ( 𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴 ) ) ) | |

8 | 5 6 7 | 3imtr4i | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵 ) ) |