Theorem disjss1 5045

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 3914	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 611	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3	2	moimdv 2546	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
4	3	alimdv 1919	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑦∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
5		dfdisj2 5041	. 2 ⊢ (Disj 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))
6		dfdisj2 5041	. 2 ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶))
7	4, 5, 6	3imtr4g 296	1 ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶))

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1537   ∈ wcel 2106  ∃*wmo 2538   ⊆ wss 3887  Disj wdisj 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-mo 2540  df-clab 2716  df-cleq 2730  df-clel 2816  df-rmo 3071  df-v 3434  df-in 3894  df-ss 3904  df-disj 5040

This theorem is referenced by:  disjeq1  5046  disjx0  5068  disjxiun  5071  disjss3  5073  volfiniun  24711  uniioovol  24743  uniioombllem4  24750  disjiunel  30935  tocyccntz  31411  carsggect  32285  carsgclctunlem2  32286  omsmeas  32290  sibfof  32307  disjf1o  42729  fsumiunss  43116  sge0iunmptlemre  43953  meadjiunlem  44003  meaiuninclem  44018