Theorem intssuni 4860

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

Assertion

Ref	Expression
intssuni	⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)

Proof of Theorem intssuni

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		r19.2z 4398	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
2	1	ex 416	. . 3 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦))
3		vex 3444	. . . 4 ⊢ 𝑥 ∈ V
4	3	elint2 4845	. . 3 ⊢ (𝑥 ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
5		eluni2 4804	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
6	2, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ≠ ∅ → (𝑥 ∈ ∩ 𝐴 → 𝑥 ∈ ∪ 𝐴))
7	6	ssrdv 3921	1 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ⊆ wss 3881  ∅c0 4243  ∪ cuni 4800  ∩ cint 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244  df-uni 4801  df-int 4839

This theorem is referenced by:  unissint  4862  intssuni2  4863  intss2  4993  fin23lem31  9754  wunint  10126  tskint  10196  incexc  15184  incexc2  15185  subgint  18295  efgval  18835  lbsextlem3  19925  cssmre  20382  uffixfr  22528  uffix2  22529  uffixsn  22530  ssmxidllem  31049  insiga  31506  dfon2lem8  33148  intidl  35467  elrfi  39635