Theorem iunss1 5006

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 4053	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 → ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶))
2		eliun 4995	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
3		eliun 4995	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)
4	1, 2, 3	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶))
5	4	ssrdv 3989	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3070   ⊆ wss 3951  ∪ ciun 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-v 3482  df-ss 3968  df-iun 4993

This theorem is referenced by:  iuneq1  5008  iunxdif2  5053  oelim2  8633  fsumiun  15857  ovolfiniun  25536  uniioovol  25614  fusgreghash2wspv  30354  ssdifidllem  33484  esum2dlem  34093  esum2d  34094  carsgclctunlem2  34321  bnj1413  35049  bnj1408  35050  volsupnfl  37672  corclrcl  43720  cotrcltrcl  43738  iuneqfzuzlem  45345  fsumiunss  45590  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  carageniuncllem1  46536  carageniuncllem2  46537  caratheodorylem2  46542  ovnsubaddlem1  46585