**Description:** Subclass relationship for class union. (Contributed by NM, 24-May-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof
shortened by JJ, 26-Jul-2021)

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

Assertion | ssuni | ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ⊆ ∪ 𝐶 ) |

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

1 | elunii | ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝑥 ∈ ∪ 𝐶 ) | |

2 | 1 | expcom | ⊢ ( 𝐵 ∈ 𝐶 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ 𝐶 ) ) |

3 | 2 | imim2d | ⊢ ( 𝐵 ∈ 𝐶 → ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝐶 ) ) ) |

4 | 3 | alimdv | ⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝐶 ) ) ) |

5 | dfss2 | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) | |

6 | dfss2 | ⊢ ( 𝐴 ⊆ ∪ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝐶 ) ) | |

7 | 4 5 6 | 3imtr4g | ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ ∪ 𝐶 ) ) |

8 | 7 | impcom | ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ⊆ ∪ 𝐶 ) |