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 | df-ss | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) | |
| 6 | df-ss | ⊢ ( 𝐴 ⊆ ∪ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝐶 ) ) | |
| 7 | 4 5 6 | 3imtr4g | ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ ∪ 𝐶 ) ) |
| 8 | 7 | impcom | ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ⊆ ∪ 𝐶 ) |