Theorem ssiun2s 5015

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 2892	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2892	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4994	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3942	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3981	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 5014	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3545	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ⊆ wss 3917  ∪ ciun 4958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-v 3452  df-ss 3934  df-iun 4960

This theorem is referenced by:  fviunfun  7926  onfununi  8313  oaordi  8513  omordi  8533  dffi3  9389  alephordi  10034  domtriomlem  10402  pwxpndom2  10625  wunex2  10698  imasaddvallem  17499  imasvscaval  17508  iundisj2  25457  voliunlem1  25458  volsup  25464  iundisj2fi  32727  constr01  33739  bnj906  34927  bnj1137  34992  bnj1408  35033  cvmliftlem10  35288  cvmliftlem13  35290  sstotbnd2  37775  mapdrvallem3  41647  onsucunifi  43366  fvmptiunrelexplb0d  43680  fvmptiunrelexplb1d  43682  corclrcl  43703  trclrelexplem  43707  corcltrcl  43735  cotrclrcl  43738  iunincfi  45095  iundjiunlem  46464  meaiuninc3v  46489  caratheodorylem1  46531  ovnhoilem1  46606