Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > intssuni | Structured version Visualization version GIF version |
Description: The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.) |
Ref | Expression |
---|---|
intssuni | ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.2z 4425 | . . . 4 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) | |
2 | 1 | ex 413 | . . 3 ⊢ (𝐴 ≠ ∅ → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦)) |
3 | vex 3436 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | elint2 4886 | . . 3 ⊢ (𝑥 ∈ ∩ 𝐴 ↔ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) |
5 | eluni2 4843 | . . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) | |
6 | 2, 4, 5 | 3imtr4g 296 | . 2 ⊢ (𝐴 ≠ ∅ → (𝑥 ∈ ∩ 𝐴 → 𝑥 ∈ ∪ 𝐴)) |
7 | 6 | ssrdv 3927 | 1 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 ⊆ wss 3887 ∅c0 4256 ∪ cuni 4839 ∩ cint 4879 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2944 df-ral 3069 df-rex 3070 df-v 3434 df-dif 3890 df-in 3894 df-ss 3904 df-nul 4257 df-uni 4840 df-int 4880 |
This theorem is referenced by: unissint 4903 intssuni2 4904 intss2 5037 fin23lem31 10099 wunint 10471 tskint 10541 incexc 15549 incexc2 15550 subgint 18779 efgval 19323 lbsextlem3 20422 cssmre 20898 uffixfr 23074 uffix2 23075 uffixsn 23076 ssmxidllem 31641 insiga 32105 dfon2lem8 33766 intidl 36187 elrfi 40516 toplatglb 46287 |
Copyright terms: Public domain | W3C validator |