Theorem ssiun2s 4974

Description: Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)

Hypothesis

Ref	Expression
ssiun2s.1	⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem ssiun2s

Step	Hyp	Ref	Expression
1		nfcv 2906	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2906	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4955	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3909	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3948	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 4973	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3502	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ⊆ wss 3883  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-v 3424  df-in 3890  df-ss 3900  df-iun 4923

This theorem is referenced by:  fviunfun  7761  onfununi  8143  oaordi  8339  omordi  8359  dffi3  9120  alephordi  9761  domtriomlem  10129  pwxpndom2  10352  wunex2  10425  imasaddvallem  17157  imasvscaval  17166  iundisj2  24618  voliunlem1  24619  volsup  24625  iundisj2fi  31020  bnj906  32810  bnj1137  32875  bnj1408  32916  cvmliftlem10  33156  cvmliftlem13  33158  sstotbnd2  35859  mapdrvallem3  39587  fvmptiunrelexplb0d  41181  fvmptiunrelexplb1d  41183  corclrcl  41204  trclrelexplem  41208  corcltrcl  41236  cotrclrcl  41239  iunincfi  42533  iundjiunlem  43887  meaiuninc3v  43912  caratheodorylem1  43954  ovnhoilem1  44029