Theorem iunssd 5014

Description: Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 8-Apr-2021.)

Hypothesis

Ref	Expression
iunssd.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
iunssd	⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Distinct variable groups:   𝑥,𝐶   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem iunssd

Step	Hyp	Ref	Expression
1		iunssd.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)
2	1	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
3		iunss 5008	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
4	2, 3	sylibr 237	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2141  ∀wral 3077   ⊆ wss 3904  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-11 2190  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3455  df-ss 3921  df-iun 4957

This theorem is referenced by:  imasaddfnlem  17581  imasaddflem  17583  subdrgint  20885  bdayiun  28084  precsexlem10  28385  gsumwrd2dccatlem  33363  constrsscn  34096  ttcmin  36951  dfttc2g  36961  oacl2g  44005  omcl2  44008  ofoaf  44030  onsucunifi  44045  meaiininclem  47148  smflim  47439  smfresal  47450  smfmullem4  47456  iunlub  49544