Theorem intssuni 4900

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 3018  ∀wral 3140  ∃wrex 3141   ⊆ wss 3938  ∅c0 4293  ∪ cuni 4840  ∩ cint 4878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954  df-nul 4294  df-uni 4841  df-int 4879

This theorem is referenced by:  unissint  4902  intssuni2  4903  fin23lem31  9767  wunint  10139  tskint  10209  incexc  15194  incexc2  15195  subgint  18305  efgval  18845  lbsextlem3  19934  cssmre  20839  uffixfr  22533  uffix2  22534  uffixsn  22535  ssmxidllem  30980  insiga  31398  dfon2lem8  33037  bj-intss  34393  intidl  35309  elrfi  39298