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

Theorem disjss1 4897
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 3846 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 601 . . . 4 (𝐴𝐵 → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
32moimdv 2555 . . 3 (𝐴𝐵 → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
43alimdv 1875 . 2 (𝐴𝐵 → (∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶) → ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶)))
5 dfdisj2 4893 . 2 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶))
6 dfdisj2 4893 . 2 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶))
74, 5, 63imtr4g 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