Theorem intssuni 4929

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 4454	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
2	1	ex 418	. . 3 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦))
3		vex 3454	. . . 4 ⊢ 𝑥 ∈ V
4	3	elint2 4913	. . 3 ⊢ (𝑥 ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
5		eluni2 4870	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
6	2, 4, 5	3imtr4g 299	. 2 ⊢ (𝐴 ≠ ∅ → (𝑥 ∈ ∩ 𝐴 → 𝑥 ∈ ∪ 𝐴))
7	6	ssrdv 3936	1 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2955  ∀wral 3076  ∃wrex 3086   ⊆ wss 3898  ∅c0 4278  ∪ cuni 4866  ∩ cint 4906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-v 3452  df-dif 3901  df-ss 3915  df-nul 4279  df-uni 4867  df-int 4907

This theorem is used by:  unissint  4931  intssuni2  4932  intss2  5067  fin23lem31  10393  wunint  10772  tskint  10842  incexc  15974  incexc2  15975  subgint  19323  efgval  19893  lbsextlem3  21400  ssdifidllem  21602  cssmre  21961  uffixfr  24204  uffix2  24205  uffixsn  24206  ssmxidllem  33932  insiga  34704  dfon2lem8  36474  intidl  38883  elrfi  43643  toplatglb  50031