Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > disjss1 | Structured version Visualization version Unicode 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 3597 | . . . . . 6 | |
2 | 1 | anim1d 588 | . . . . 5 |
3 | 2 | alrimiv 1855 | . . . 4 |
4 | moim 2519 | . . . 4 | |
5 | 3, 4 | syl 17 | . . 3 |
6 | 5 | alimdv 1845 | . 2 |
7 | dfdisj2 4622 | . 2 Disj | |
8 | dfdisj2 4622 | . 2 Disj | |
9 | 6, 7, 8 | 3imtr4g 285 | 1 Disj Disj |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wal 1481 wcel 1990 wmo 2471 wss 3574 Disj wdisj 4620 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-rmo 2920 df-in 3581 df-ss 3588 df-disj 4621 |
This theorem is referenced by: disjeq1 4627 disjx0 4647 disjxiun 4649 disjxiunOLD 4650 disjss3 4652 volfiniun 23315 uniioovol 23347 uniioombllem4 23354 disjiunel 29409 carsggect 30380 carsgclctunlem2 30381 omsmeas 30385 sibfof 30402 disjf1o 39378 fsumiunss 39807 sge0iunmptlemre 40632 meadjiunlem 40682 meaiuninclem 40697 |
Copyright terms: Public domain | W3C validator |