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

Theorem disjss1 4553
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 3561 . . . . . 6 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 585 . . . . 5 (𝐴𝐵 → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
32alrimiv 1841 . . . 4 (𝐴𝐵 → ∀𝑥((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
4 moim 2506 . . . 4 (∀𝑥((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)) → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
53, 4syl 17 . . 3 (𝐴𝐵 → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
65alimdv 1831 . 2 (𝐴𝐵 → (∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶) → ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶)))
7 dfdisj2 4549 . 2 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶))
8 dfdisj2 4549 . 2 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶))
96, 7, 83imtr4g 283 1 (𝐴𝐵 → (Disj 𝑥𝐵 𝐶Disj 𝑥𝐴 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wal 1472  wcel 1976  ∃*wmo 2458  wss 3539  Disj wdisj 4547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-rmo 2903  df-in 3546  df-ss 3553  df-disj 4548
This theorem is referenced by:  disjeq1  4554  disjx0  4571  disjxiun  4573  disjxiunOLD  4574  disjss3  4576  volfiniun  23039  uniioovol  23070  uniioombllem4  23077  disjiunel  28597  carsggect  29513  carsgclctunlem2  29514  omsmeas  29518  sibfof  29535  disjf1o  38169  fsumiunss  38439  sge0iunmptlemre  39105  meadjiunlem  39155  meaiuninclem  39170
  Copyright terms: Public domain W3C validator