**Description:** The intersection of a nonempty set is a subclass of its union.
(Contributed by NM, 29-Jul-2006)

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

Assertion | intssuni | ⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴 ) |

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

1 | r19.2z | ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) | |

2 | 1 | ex | ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) ) |

3 | vex | ⊢ 𝑥 ∈ V | |

4 | 3 | elint2 | ⊢ ( 𝑥 ∈ ∩ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) |

5 | eluni2 | ⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) | |

6 | 2 4 5 | 3imtr4g | ⊢ ( 𝐴 ≠ ∅ → ( 𝑥 ∈ ∩ 𝐴 → 𝑥 ∈ ∪ 𝐴 ) ) |

7 | 6 | ssrdv | ⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴 ) |