Theorem ssiun2s 4978

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 2901	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2901	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4957	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3908	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3946	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 4977	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3519	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ⊆ wss 3883  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-v 3433  df-ss 3900  df-iun 4923

This theorem is referenced by:  fviunfun  7887  onfununi  8271  oaordi  8471  omordi  8491  dffi3  9334  alephordi  9987  domtriomlem  10355  pwxpndom2  10579  wunex2  10652  imasaddvallem  17484  imasvscaval  17493  iundisj2  25534  voliunlem1  25535  volsup  25541  iundisj2fi  32889  constr01  33926  bnj906  35112  bnj1137  35177  bnj1408  35218  cvmliftlem10  35522  cvmliftlem13  35524  ttciunun  36739  sstotbnd2  38141  mapdrvallem3  42138  onsucunifi  43815  fvmptiunrelexplb0d  44128  fvmptiunrelexplb1d  44130  corclrcl  44151  trclrelexplem  44155  corcltrcl  44183  cotrclrcl  44186  iunincfi  45541  iundjiunlem  46902  meaiuninc3v  46927  caratheodorylem1  46969  ovnhoilem1  47044