Description: A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | ssun | ⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) → 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun3 | ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ) | |
2 | ssun4 | ⊢ ( 𝐴 ⊆ 𝐶 → 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ) | |
3 | 1 2 | jaoi | ⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) → 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ) |