Theorem disjss1 4818

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.

Step	Hyp	Ref	Expression
1		ssel 3792	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 600	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3	2	moimd 2684	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
4	3	alimdv 2007	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑦∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
5		dfdisj2 4814	. 2 ⊢ (Disj 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))
6		dfdisj2 4814	. 2 ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶))
7	4, 5, 6	3imtr4g 287	1 ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶))

Syntax hints:   → wi 4   ∧ wa 384  ∀wal 1635   ∈ wcel 2156  ∃*wmo 2631   ⊆ wss 3769  Disj wdisj 4812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-rmo 3104  df-in 3776  df-ss 3783  df-disj 4813

This theorem is referenced by:  disjeq1  4819  disjx0  4839  disjxiun  4841  disjss3  4843  volfiniun  23528  uniioovol  23560  uniioombllem4  23567  disjiunel  29734  carsggect  30705  carsgclctunlem2  30706  omsmeas  30710  sibfof  30727  disjf1o  39867  fsumiunss  40287  sge0iunmptlemre  41111  meadjiunlem  41161  meaiuninclem  41176