Theorem iunss1 4918

Description: Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem iunss1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssrexv 3968	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 → ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶))
2		eliun 4908	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
3		eliun 4908	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)
4	1, 2, 3	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶))
5	4	ssrdv 3907	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2110  ∃wrex 3062   ⊆ wss 3866  ∪ ciun 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-v 3410  df-in 3873  df-ss 3883  df-iun 4906

This theorem is referenced by:  iuneq1  4920  iunxdif2  4962  oelim2  8323  fsumiun  15385  ovolfiniun  24398  uniioovol  24476  fusgreghash2wspv  28418  esum2dlem  31772  esum2d  31773  carsgclctunlem2  31998  bnj1413  32728  bnj1408  32729  volsupnfl  35559  corclrcl  40992  cotrcltrcl  41010  iuneqfzuzlem  42546  fsumiunss  42791  sge0iunmptlemfi  43626  sge0iunmptlemre  43628  carageniuncllem1  43734  carageniuncllem2  43735  caratheodorylem2  43740  ovnsubaddlem1  43783