Theorem ssiun2s 4964

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 2977	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2977	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4945	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3959	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3997	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 4963	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3572	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110   ⊆ wss 3935  ∪ ciun 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-in 3942  df-ss 3951  df-iun 4913

This theorem is referenced by:  fviunfun  7640  onfununi  7972  oaordi  8166  omordi  8186  dffi3  8889  alephordi  9494  domtriomlem  9858  pwxpndom2  10081  wunex2  10154  imasaddvallem  16796  imasvscaval  16805  iundisj2  24144  voliunlem1  24145  volsup  24151  iundisj2fi  30514  bnj906  32197  bnj1137  32262  bnj1408  32303  cvmliftlem10  32536  cvmliftlem13  32538  sstotbnd2  35046  mapdrvallem3  38776  fvmptiunrelexplb0d  40022  fvmptiunrelexplb1d  40024  corclrcl  40045  trclrelexplem  40049  corcltrcl  40077  cotrclrcl  40080  iunincfi  41353  iundjiunlem  42735  meaiuninc3v  42760  caratheodorylem1  42802  ovnhoilem1  42877