Theorem ssiun2s 5017

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 2931	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2931	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4996	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3938	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3976	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 5016	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3549	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   ⊆ wss 3913  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-v 3465  df-ss 3930  df-iun 4962

This theorem is referenced by:  fviunfun  7942  onfununi  8328  oaordi  8531  omordi  8551  dffi3  9391  alephordi  10058  domtriomlem  10426  pwxpndom2  10650  wunex2  10723  imasaddvallem  17583  imasvscaval  17592  iundisj2  25677  voliunlem1  25678  volsup  25684  iundisj2fi  33083  constr01  34077  bnj906  35263  bnj1137  35328  bnj1408  35369  cvmliftlem10  35685  cvmliftlem13  35687  ttciunun  36911  sstotbnd2  38313  mapdrvallem3  42310  onsucunifi  43989  fvmptiunrelexplb0d  44302  fvmptiunrelexplb1d  44304  corclrcl  44325  trclrelexplem  44329  corcltrcl  44357  cotrclrcl  44360  iunincfi  45704  iundjiunlem  47065  meaiuninc3v  47090  caratheodorylem1  47132  ovnhoilem1  47207