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

Theorem disjss1 5023
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 3946 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 613 . . . 4 (𝐴𝐵 → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
32moimdv 2630 . . 3 (𝐴𝐵 → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
43alimdv 1918 . 2 (𝐴𝐵 → (∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶) → ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶)))
5 dfdisj2 5019 . 2 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶))
6 dfdisj2 5019 . 2 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶))
74, 5, 63imtr4g 299 1 (𝐴𝐵 → (Disj 𝑥𝐵 𝐶Disj 𝑥𝐴 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wal 1536  wcel 2115  ∃*wmo 2622  wss 3919  Disj wdisj 5017
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-mo 2624  df-clab 2803  df-cleq 2817  df-clel 2896  df-rmo 3141  df-v 3482  df-in 3926  df-ss 3936  df-disj 5018
This theorem is referenced by:  disjeq1  5024  disjx0  5046  disjxiun  5049  disjss3  5051  volfiniun  24157  uniioovol  24189  uniioombllem4  24196  disjiunel  30360  tocyccntz  30821  carsggect  31636  carsgclctunlem2  31637  omsmeas  31641  sibfof  31658  disjf1o  41747  fsumiunss  42147  sge0iunmptlemre  42984  meadjiunlem  43034  meaiuninclem  43049
  Copyright terms: Public domain W3C validator