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

Theorem disjss1 4760
 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 3746 . . . . . 6 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 598 . . . . 5 (𝐴𝐵 → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
32alrimiv 2007 . . . 4 (𝐴𝐵 → ∀𝑥((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
4 moim 2668 . . . 4 (∀𝑥((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)) → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
53, 4syl 17 . . 3 (𝐴𝐵 → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
65alimdv 1997 . 2 (𝐴𝐵 → (∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶) → ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶)))
7 dfdisj2 4756 . 2 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶))
8 dfdisj2 4756 . 2 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶))
96, 7, 83imtr4g 285 1 (𝐴𝐵 → (Disj 𝑥𝐵 𝐶Disj 𝑥𝐴 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382  ∀wal 1629   ∈ wcel 2145  ∃*wmo 2619   ⊆ wss 3723  Disj wdisj 4754 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-rmo 3069  df-in 3730  df-ss 3737  df-disj 4755 This theorem is referenced by:  disjeq1  4761  disjx0  4781  disjxiun  4783  disjss3  4785  volfiniun  23535  uniioovol  23567  uniioombllem4  23574  disjiunel  29747  carsggect  30720  carsgclctunlem2  30721  omsmeas  30725  sibfof  30742  disjf1o  39898  fsumiunss  40325  sge0iunmptlemre  41149  meadjiunlem  41199  meaiuninclem  41214
 Copyright terms: Public domain W3C validator