![]() |
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 3846 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 601 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
3 | 2 | moimdv 2555 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶))) |
4 | 3 | alimdv 1875 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑦∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶))) |
5 | dfdisj2 4893 | . 2 ⊢ (Disj 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) | |
6 | dfdisj2 4893 | . 2 ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)) | |
7 | 4, 5, 6 | 3imtr4g 288 | 1 ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∀wal 1505 ∈ wcel 2050 ∃*wmo 2545 ⊆ wss 3823 Disj wdisj 4891 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-clab 2753 df-cleq 2765 df-clel 2840 df-rmo 3090 df-in 3830 df-ss 3837 df-disj 4892 |
This theorem is referenced by: disjeq1 4898 disjx0 4918 disjxiun 4920 disjss3 4922 volfiniun 23845 uniioovol 23877 uniioombllem4 23884 disjiunel 30106 carsggect 31221 carsgclctunlem2 31222 omsmeas 31226 sibfof 31243 disjf1o 40876 fsumiunss 41287 sge0iunmptlemre 42128 meadjiunlem 42178 meaiuninclem 42193 |
Copyright terms: Public domain | W3C validator |