Theorem disjss1 5079

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 3907	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 623	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3	2	moimdv 2574	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
4	3	alimdv 1950	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑦∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
5		dfdisj2 5075	. 2 ⊢ (Disj 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))
6		dfdisj2 5075	. 2 ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶))
7	4, 5, 6	3imtr4g 299	1 ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1567   ∈ wcel 2146  ∃*wmo 2565   ⊆ wss 3900  Disj wdisj 5073

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-mo 2567  df-clel 2839  df-rmo 3369  df-ss 3901  df-disj 5074

This theorem is used by:  disjeq1  5080  disjx0  5101  disjxiun  5103  disjss3  5105  volfiniun  25883  uniioovol  25915  uniioombllem4  25922  disjiunel  33247  tocyccntz  33761  carsggect  35006  carsgclctunlem2  35007  omsmeas  35011  sibfof  35028  disjf1o  46351  fsumiunss  46732  sge0iunmptlemre  47570  meadjiunlem  47620  meaiuninclem  47635