Theorem intssuni 4994

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 4518	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
2	1	ex 412	. . 3 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦))
3		vex 3492	. . . 4 ⊢ 𝑥 ∈ V
4	3	elint2 4977	. . 3 ⊢ (𝑥 ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
5		eluni2 4935	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
6	2, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ≠ ∅ → (𝑥 ∈ ∩ 𝐴 → 𝑥 ∈ ∪ 𝐴))
7	6	ssrdv 4014	1 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076   ⊆ wss 3976  ∅c0 4352  ∪ cuni 4931  ∩ cint 4970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-v 3490  df-dif 3979  df-ss 3993  df-nul 4353  df-uni 4932  df-int 4971

This theorem is referenced by:  unissint  4996  intssuni2  4997  intss2  5131  fin23lem31  10412  wunint  10784  tskint  10854  incexc  15885  incexc2  15886  subgint  19190  efgval  19759  lbsextlem3  21185  cssmre  21734  uffixfr  23952  uffix2  23953  uffixsn  23954  ssdifidllem  33449  ssmxidllem  33466  insiga  34101  dfon2lem8  35754  intidl  37989  elrfi  42650  toplatglb  48673