Theorem ss2iun 4967

Description: Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

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

Proof of Theorem ss2iun

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3929	. . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
2	1	ralimi 3075	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
3		rexim 3079	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶))
4	2, 3	syl 17	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶))
5		eliun 4952	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
6		eliun 4952	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
7	4, 5, 6	3imtr4g 296	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶))
8	7	ssrdv 3941	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062   ⊆ wss 3903  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3444  df-ss 3920  df-iun 4950

This theorem is referenced by:  iuneq2  4968  abnexg  7711  oawordri  8487  omwordri  8509  oewordri  8530  oeworde  8531  r1val1  9710  cfslb2n  10190  imasaddvallem  17462  dprdss  19972  tgcmp  23357  txcmplem1  23597  txcmplem2  23598  xkococnlem  23615  alexsubALT  24007  ptcmplem3  24010  metnrmlem2  24817  uniiccvol  25549  dvfval  25866  gsumpart  33157  bnj1145  35169  bnj1136  35173  tz9.1regs  35312  filnetlem3  36596  poimirlem32  37903  sstotbnd2  38025  equivtotbnd  38029  trclrelexplem  44067  corcltrcl  44095  cotrclrcl  44098  ovolval5lem2  47011  ovolval5lem3  47012  smflimsuplem7  47184