Theorem ssiun2s 4717

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 2903	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2903	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4703	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3738	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3774	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 4716	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3412	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2140   ⊆ wss 3716  ∪ ciun 4673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-v 3343  df-in 3723  df-ss 3730  df-iun 4675

This theorem is referenced by:  onfununi  7609  oaordi  7798  omordi  7818  dffi3  8505  alephordi  9108  domtriomlem  9477  pwxpndom2  9700  wunex2  9773  imasaddvallem  16412  imasvscaval  16421  iundisj2  23538  voliunlem1  23539  volsup  23545  iundisj2fi  29887  bnj906  31329  bnj1137  31392  bnj1408  31433  cvmliftlem10  31605  cvmliftlem13  31607  sstotbnd2  33905  mapdrvallem3  37456  fvmptiunrelexplb0d  38497  fvmptiunrelexplb1d  38499  corclrcl  38520  trclrelexplem  38524  corcltrcl  38552  cotrclrcl  38555  iunincfi  39790  iundjiunlem  41198  meaiuninc3v  41223  caratheodorylem1  41265  ovnhoilem1  41340