Theorem ssiun2s 5071

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 5050	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 4001	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 4040	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 5070	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3588	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ⊆ wss 3976  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-v 3490  df-ss 3993  df-iun 5017

This theorem is referenced by:  fviunfun  7985  onfununi  8397  oaordi  8602  omordi  8622  dffi3  9500  alephordi  10143  domtriomlem  10511  pwxpndom2  10734  wunex2  10807  imasaddvallem  17589  imasvscaval  17598  iundisj2  25603  voliunlem1  25604  volsup  25610  iundisj2fi  32802  constr01  33732  bnj906  34906  bnj1137  34971  bnj1408  35012  cvmliftlem10  35262  cvmliftlem13  35264  sstotbnd2  37734  mapdrvallem3  41603  onsucunifi  43332  fvmptiunrelexplb0d  43646  fvmptiunrelexplb1d  43648  corclrcl  43669  trclrelexplem  43673  corcltrcl  43701  cotrclrcl  43704  iunincfi  44996  iundjiunlem  46380  meaiuninc3v  46405  caratheodorylem1  46447  ovnhoilem1  46522