Theorem ssiun2s 5009

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 2925	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2925	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4988	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3905	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3943	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 5008	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3538	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146   ⊆ wss 3899  ∪ ciun 4953

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-v 3455  df-ss 3900  df-iun 4955

This theorem is used by:  fviunfun  7964  onfununi  8360  oaordi  8565  omordi  8585  dffi3  9433  alephordi  10163  domtriomlem  10530  pwxpndom2  10760  wunex2  10833  imasaddvallem  17713  imasvscaval  17722  iundisj2  25882  voliunlem1  25883  volsup  25889  iundisj2fi  33442  constr01  34427  bnj906  35613  bnj1137  35678  bnj1408  35719  ptpconn  36119  cvmliftlem10  36180  cvmliftlem13  36182  ttciunun  37426  sstotbnd2  38848  mapdrvallem3  42843  onsucunifi  44512  fvmptiunrelexplb0d  44824  fvmptiunrelexplb1d  44826  corclrcl  44847  trclrelexplem  44851  corcltrcl  44879  cotrclrcl  44882  iunincfi  46248  iundjiunlem  47608  meaiuninc3v  47633  caratheodorylem1  47675  ovnhoilem1  47750