Theorem ssiun2s 4784

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 2969	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2969	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4770	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3820	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3857	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 4783	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3488	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1658   ∈ wcel 2166   ⊆ wss 3798  ∪ ciun 4740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-v 3416  df-in 3805  df-ss 3812  df-iun 4742

This theorem is referenced by:  onfununi  7704  oaordi  7893  omordi  7913  dffi3  8606  alephordi  9210  domtriomlem  9579  pwxpndom2  9802  wunex2  9875  imasaddvallem  16542  imasvscaval  16551  iundisj2  23715  voliunlem1  23716  volsup  23722  iundisj2fi  30103  bnj906  31546  bnj1137  31609  bnj1408  31650  cvmliftlem10  31822  cvmliftlem13  31824  sstotbnd2  34115  mapdrvallem3  37721  fvmptiunrelexplb0d  38817  fvmptiunrelexplb1d  38819  corclrcl  38840  trclrelexplem  38844  corcltrcl  38872  cotrclrcl  38875  iunincfi  40089  iundjiunlem  41467  meaiuninc3v  41492  caratheodorylem1  41534  ovnhoilem1  41609