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

Theorem disjss1 4559
 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 3562 . . . . . 6 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 586 . . . . 5 (𝐴𝐵 → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
32alrimiv 1842 . . . 4 (𝐴𝐵 → ∀𝑥((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
4 moim 2507 . . . 4 (∀𝑥((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)) → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
53, 4syl 17 . . 3 (𝐴𝐵 → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
65alimdv 1832 . 2 (𝐴𝐵 → (∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶) → ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶)))
7 dfdisj2 4555 . 2 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶))
8 dfdisj2 4555 . 2 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶))
96, 7, 83imtr4g 284 1 (𝐴𝐵 → (Disj 𝑥𝐵 𝐶Disj 𝑥𝐴 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1473   ∈ wcel 1977  ∃*wmo 2459   ⊆ wss 3540  Disj wdisj 4553 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-rmo 2904  df-in 3547  df-ss 3554  df-disj 4554 This theorem is referenced by:  disjeq1  4560  disjx0  4577  disjxiun  4579  disjxiunOLD  4580  disjss3  4582  volfiniun  23122  uniioovol  23153  uniioombllem4  23160  disjiunel  28791  carsggect  29707  carsgclctunlem2  29708  omsmeas  29712  sibfof  29729  disjf1o  38373  fsumiunss  38642  sge0iunmptlemre  39308  meadjiunlem  39358  meaiuninclem  39373
 Copyright terms: Public domain W3C validator