Theorem ssiun2s 5013

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 2925	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2925	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4992	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3930	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3968	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 5012	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3540	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ⊆ wss 3905  ∪ ciun 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-v 3457  df-ss 3922  df-iun 4958

This theorem is referenced by:  fviunfun  7938  onfununi  8324  oaordi  8527  omordi  8547  dffi3  9387  alephordi  10054  domtriomlem  10421  pwxpndom2  10645  wunex2  10718  imasaddvallem  17578  imasvscaval  17587  iundisj2  25708  voliunlem1  25709  volsup  25715  iundisj2fi  33142  constr01  34132  bnj906  35318  bnj1137  35383  bnj1408  35424  cvmliftlem10  35786  cvmliftlem13  35788  ttciunun  37042  sstotbnd2  38445  mapdrvallem3  42440  onsucunifi  44117  fvmptiunrelexplb0d  44430  fvmptiunrelexplb1d  44432  corclrcl  44453  trclrelexplem  44457  corcltrcl  44485  cotrclrcl  44488  iunincfi  45832  iundjiunlem  47193  meaiuninc3v  47218  caratheodorylem1  47260  ovnhoilem1  47335