Theorem ss2iun 5010

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 3977	. . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
2	1	ralimi 3083	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
3		rexim 3087	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶))
4	2, 3	syl 17	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶))
5		eliun 4995	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
6		eliun 4995	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
7	4, 5, 6	3imtr4g 296	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶))
8	7	ssrdv 3989	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3061  ∃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-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-iun 4993

This theorem is referenced by:  iuneq2  5011  abnexg  7776  oawordri  8588  omwordri  8610  oewordri  8630  oeworde  8631  r1val1  9826  cfslb2n  10308  imasaddvallem  17574  dprdss  20049  tgcmp  23409  txcmplem1  23649  txcmplem2  23650  xkococnlem  23667  alexsubALT  24059  ptcmplem3  24062  metnrmlem2  24882  uniiccvol  25615  dvfval  25932  gsumpart  33060  bnj1145  35007  bnj1136  35011  filnetlem3  36381  poimirlem32  37659  sstotbnd2  37781  equivtotbnd  37785  trclrelexplem  43724  corcltrcl  43752  cotrclrcl  43755  ovolval5lem2  46668  ovolval5lem3  46669  smflimsuplem7  46841