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

Theorem disjss1 5116
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 3977 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 611 . . . 4 (𝐴𝐵 → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
32moimdv 2546 . . 3 (𝐴𝐵 → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
43alimdv 1916 . 2 (𝐴𝐵 → (∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶) → ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶)))
5 dfdisj2 5112 . 2 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶))
6 dfdisj2 5112 . 2 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶))
74, 5, 63imtr4g 296 1 (𝐴𝐵 → (Disj 𝑥𝐵 𝐶Disj 𝑥𝐴 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1538  wcel 2108  ∃*wmo 2538  wss 3951  Disj wdisj 5110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540  df-clel 2816  df-rmo 3380  df-ss 3968  df-disj 5111
This theorem is referenced by:  disjeq1  5117  disjx0  5138  disjxiun  5140  disjss3  5142  volfiniun  25582  uniioovol  25614  uniioombllem4  25621  disjiunel  32609  tocyccntz  33164  carsggect  34320  carsgclctunlem2  34321  omsmeas  34325  sibfof  34342  disjf1o  45196  fsumiunss  45590  sge0iunmptlemre  46430  meadjiunlem  46480  meaiuninclem  46495
  Copyright terms: Public domain W3C validator