Theorem ssiun2s 4991

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 2898	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2898	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4969	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3914	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3953	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 4990	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3519	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-v 3431  df-ss 3906  df-iun 4935

This theorem is referenced by:  fviunfun  7898  onfununi  8281  oaordi  8481  omordi  8501  dffi3  9344  alephordi  9996  domtriomlem  10364  pwxpndom2  10588  wunex2  10661  imasaddvallem  17493  imasvscaval  17502  iundisj2  25516  voliunlem1  25517  volsup  25523  iundisj2fi  32870  constr01  33886  bnj906  35072  bnj1137  35137  bnj1408  35178  cvmliftlem10  35476  cvmliftlem13  35478  ttciunun  36693  sstotbnd2  38095  mapdrvallem3  42092  onsucunifi  43798  fvmptiunrelexplb0d  44111  fvmptiunrelexplb1d  44113  corclrcl  44134  trclrelexplem  44138  corcltrcl  44166  cotrclrcl  44169  iunincfi  45524  iundjiunlem  46887  meaiuninc3v  46912  caratheodorylem1  46954  ovnhoilem1  47029