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

Theorem disjss1 5075
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 3936 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 612 . . . 4 (𝐴𝐵 → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
32moimdv 2546 . . 3 (𝐴𝐵 → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
43alimdv 1920 . 2 (𝐴𝐵 → (∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶) → ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶)))
5 dfdisj2 5071 . 2 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶))
6 dfdisj2 5071 . 2 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶))
74, 5, 63imtr4g 296 1 (𝐴𝐵 → (Disj 𝑥𝐵 𝐶Disj 𝑥𝐴 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wal 1540  wcel 2107  ∃*wmo 2538  wss 3909  Disj wdisj 5069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2730  df-clel 2816  df-rmo 3352  df-v 3446  df-in 3916  df-ss 3926  df-disj 5070
This theorem is referenced by:  disjeq1  5076  disjx0  5098  disjxiun  5101  disjss3  5103  volfiniun  24839  uniioovol  24871  uniioombllem4  24878  disjiunel  31318  tocyccntz  31794  carsggect  32698  carsgclctunlem2  32699  omsmeas  32703  sibfof  32720  disjf1o  43205  fsumiunss  43607  sge0iunmptlemre  44447  meadjiunlem  44497  meaiuninclem  44512
  Copyright terms: Public domain W3C validator