Theorem intssuni 4922

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 4447	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
2	1	ex 415	. . 3 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦))
3		vex 3452	. . . 4 ⊢ 𝑥 ∈ V
4	3	elint2 4906	. . 3 ⊢ (𝑥 ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
5		eluni2 4863	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)
6	2, 4, 5	3imtr4g 298	. 2 ⊢ (𝐴 ≠ ∅ → (𝑥 ∈ ∩ 𝐴 → 𝑥 ∈ ∪ 𝐴))
7	6	ssrdv 3937	1 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2136   ≠ wne 2951  ∀wral 3070  ∃wrex 3080   ⊆ wss 3899  ∅c0 4280  ∪ cuni 4859  ∩ cint 4899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rex 3081  df-v 3450  df-dif 3902  df-ss 3916  df-nul 4281  df-uni 4860  df-int 4900

This theorem is referenced by:  unissint  4924  intssuni2  4925  intss2  5059  fin23lem31  10290  wunint  10663  tskint  10733  incexc  15843  incexc2  15844  subgint  19168  efgval  19733  lbsextlem3  21203  cssmre  21718  uffixfr  23956  uffix2  23957  uffixsn  23958  ssdifidllem  33597  ssmxidllem  33615  insiga  34388  dfon2lem8  36086  intidl  38476  elrfi  43223  toplatglb  49570