Theorem ssiun2s 4992

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 2899	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2899	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4970	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3915	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3954	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 4991	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3520	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890  ∪ ciun 4934

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-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-v 3432  df-ss 3907  df-iun 4936

This theorem is referenced by:  fviunfun  7892  onfununi  8275  oaordi  8475  omordi  8495  dffi3  9338  alephordi  9990  domtriomlem  10358  pwxpndom2  10582  wunex2  10655  imasaddvallem  17487  imasvscaval  17496  iundisj2  25529  voliunlem1  25530  volsup  25536  iundisj2fi  32888  constr01  33905  bnj906  35091  bnj1137  35156  bnj1408  35197  cvmliftlem10  35495  cvmliftlem13  35497  ttciunun  36712  sstotbnd2  38112  mapdrvallem3  42109  onsucunifi  43819  fvmptiunrelexplb0d  44132  fvmptiunrelexplb1d  44134  corclrcl  44155  trclrelexplem  44159  corcltrcl  44187  cotrclrcl  44190  iunincfi  45545  iundjiunlem  46908  meaiuninc3v  46933  caratheodorylem1  46975  ovnhoilem1  47050