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  7889  onfununi  8272  oaordi  8472  omordi  8492  dffi3  9335  alephordi  9985  domtriomlem  10353  pwxpndom2  10577  wunex2  10650  imasaddvallem  17482  imasvscaval  17491  iundisj2  25524  voliunlem1  25525  volsup  25531  iundisj2fi  32883  constr01  33900  bnj906  35086  bnj1137  35151  bnj1408  35192  cvmliftlem10  35490  cvmliftlem13  35492  ttciunun  36707  sstotbnd2  38099  mapdrvallem3  42096  onsucunifi  43806  fvmptiunrelexplb0d  44119  fvmptiunrelexplb1d  44121  corclrcl  44142  trclrelexplem  44146  corcltrcl  44174  cotrclrcl  44177  iunincfi  45532  iundjiunlem  46895  meaiuninc3v  46920  caratheodorylem1  46962  ovnhoilem1  47037