Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjss1 Structured version   Visualization version   Unicode version

Theorem disjss1 4382
 Description: A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
Assertion
Ref Expression
disjss1 Disj Disj
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem disjss1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ssel 3428 . . . . . 6
21anim1d 568 . . . . 5
32alrimiv 1775 . . . 4
4 moim 2350 . . . 4
53, 4syl 17 . . 3
65alimdv 1765 . 2
7 dfdisj2 4378 . 2 Disj
8 dfdisj2 4378 . 2 Disj
96, 7, 83imtr4g 274 1 Disj Disj
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371  wal 1444   wcel 1889  wmo 2302   wss 3406  Disj wdisj 4376 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433 This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-rmo 2747  df-in 3413  df-ss 3420  df-disj 4377 This theorem is referenced by:  disjeq1  4383  disjx0  4400  disjxiun  4402  disjss3  4404  volfiniun  22512  uniioovol  22548  uniioombllem4  22556  disjiunel  28218  carsggect  29162  carsgclctunlem2  29163  omsmeas  29167  omsmeasOLD  29168  sibfof  29185  disjf1o  37476  fsumiunss  37664  sge0iunmptlemre  38267  meadjiunlem  38313
 Copyright terms: Public domain W3C validator