Theorem ssiun2s 4979

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ⊆ wss 3888  ∪ ciun 4925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-v 3435  df-in 3895  df-ss 3905  df-iun 4927

This theorem is referenced by:  fviunfun  7796  onfununi  8181  oaordi  8386  omordi  8406  dffi3  9199  alephordi  9839  domtriomlem  10207  pwxpndom2  10430  wunex2  10503  imasaddvallem  17249  imasvscaval  17258  iundisj2  24722  voliunlem1  24723  volsup  24729  iundisj2fi  31127  bnj906  32919  bnj1137  32984  bnj1408  33025  cvmliftlem10  33265  cvmliftlem13  33267  sstotbnd2  35941  mapdrvallem3  39667  fvmptiunrelexplb0d  41299  fvmptiunrelexplb1d  41301  corclrcl  41322  trclrelexplem  41326  corcltrcl  41354  cotrclrcl  41357  iunincfi  42651  iundjiunlem  44004  meaiuninc3v  44029  caratheodorylem1  44071  ovnhoilem1  44146