Theorem ssiun2s 4974

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 2979	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2979	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4955	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3962	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 4000	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 4973	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3575	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   ⊆ wss 3938  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-v 3498  df-in 3945  df-ss 3954  df-iun 4923

This theorem is referenced by:  fviunfun  7648  onfununi  7980  oaordi  8174  omordi  8194  dffi3  8897  alephordi  9502  domtriomlem  9866  pwxpndom2  10089  wunex2  10162  imasaddvallem  16804  imasvscaval  16813  iundisj2  24152  voliunlem1  24153  volsup  24159  iundisj2fi  30522  bnj906  32204  bnj1137  32269  bnj1408  32310  cvmliftlem10  32543  cvmliftlem13  32545  sstotbnd2  35054  mapdrvallem3  38784  fvmptiunrelexplb0d  40036  fvmptiunrelexplb1d  40038  corclrcl  40059  trclrelexplem  40063  corcltrcl  40091  cotrclrcl  40094  iunincfi  41367  iundjiunlem  42748  meaiuninc3v  42773  caratheodorylem1  42815  ovnhoilem1  42890