![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > disjss1 | Structured version Visualization version GIF version |
Description: A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
Ref | Expression |
---|---|
disjss1 | ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3908 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 613 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
3 | 2 | moimdv 2604 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶))) |
4 | 3 | alimdv 1917 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑦∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶))) |
5 | dfdisj2 4997 | . 2 ⊢ (Disj 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) | |
6 | dfdisj2 4997 | . 2 ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)) | |
7 | 4, 5, 6 | 3imtr4g 299 | 1 ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∀wal 1536 ∈ wcel 2111 ∃*wmo 2596 ⊆ wss 3881 Disj wdisj 4995 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-mo 2598 df-clab 2777 df-cleq 2791 df-clel 2870 df-rmo 3114 df-v 3443 df-in 3888 df-ss 3898 df-disj 4996 |
This theorem is referenced by: disjeq1 5002 disjx0 5024 disjxiun 5027 disjss3 5029 volfiniun 24151 uniioovol 24183 uniioombllem4 24190 disjiunel 30359 tocyccntz 30836 carsggect 31686 carsgclctunlem2 31687 omsmeas 31691 sibfof 31708 disjf1o 41818 fsumiunss 42217 sge0iunmptlemre 43054 meadjiunlem 43104 meaiuninclem 43119 |
Copyright terms: Public domain | W3C validator |