Theorem ssiun2s 5006

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 4984	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3928	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3967	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 5005	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3533	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ⊆ 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-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 3444  df-ss 3920  df-iun 4950

This theorem is referenced by:  fviunfun  7899  onfununi  8283  oaordi  8483  omordi  8503  dffi3  9346  alephordi  9996  domtriomlem  10364  pwxpndom2  10588  wunex2  10661  imasaddvallem  17462  imasvscaval  17471  iundisj2  25518  voliunlem1  25519  volsup  25525  iundisj2fi  32888  constr01  33920  bnj906  35106  bnj1137  35171  bnj1408  35212  cvmliftlem10  35510  cvmliftlem13  35512  sstotbnd2  38025  mapdrvallem3  42022  onsucunifi  43727  fvmptiunrelexplb0d  44040  fvmptiunrelexplb1d  44042  corclrcl  44063  trclrelexplem  44067  corcltrcl  44095  cotrclrcl  44098  iunincfi  45453  iundjiunlem  46817  meaiuninc3v  46842  caratheodorylem1  46884  ovnhoilem1  46959