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

Theorem disjss1 4778
 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 3738 . . . . . 6 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 589 . . . . 5 (𝐴𝐵 → ((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
32alrimiv 2004 . . . 4 (𝐴𝐵 → ∀𝑥((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)))
4 moim 2657 . . . 4 (∀𝑥((𝑥𝐴𝑦𝐶) → (𝑥𝐵𝑦𝐶)) → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
53, 4syl 17 . . 3 (𝐴𝐵 → (∃*𝑥(𝑥𝐵𝑦𝐶) → ∃*𝑥(𝑥𝐴𝑦𝐶)))
65alimdv 1994 . 2 (𝐴𝐵 → (∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶) → ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶)))
7 dfdisj2 4774 . 2 (Disj 𝑥𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐵𝑦𝐶))
8 dfdisj2 4774 . 2 (Disj 𝑥𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥𝐴𝑦𝐶))
96, 7, 83imtr4g 285 1 (𝐴𝐵 → (Disj 𝑥𝐵 𝐶Disj 𝑥𝐴 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1630   ∈ wcel 2139  ∃*wmo 2608   ⊆ wss 3715  Disj wdisj 4772 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-rmo 3058  df-in 3722  df-ss 3729  df-disj 4773 This theorem is referenced by:  disjeq1  4779  disjx0  4799  disjxiun  4801  disjss3  4803  volfiniun  23535  uniioovol  23567  uniioombllem4  23574  disjiunel  29737  carsggect  30710  carsgclctunlem2  30711  omsmeas  30715  sibfof  30732  disjf1o  39895  fsumiunss  40328  sge0iunmptlemre  41153  meadjiunlem  41203  meaiuninclem  41218
 Copyright terms: Public domain W3C validator