Theorem ssiun2s 5012

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 2891	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2891	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4991	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3939	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3978	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 5011	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3542	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-v 3449  df-ss 3931  df-iun 4957

This theorem is referenced by:  fviunfun  7923  onfununi  8310  oaordi  8510  omordi  8530  dffi3  9382  alephordi  10027  domtriomlem  10395  pwxpndom2  10618  wunex2  10691  imasaddvallem  17492  imasvscaval  17501  iundisj2  25450  voliunlem1  25451  volsup  25457  iundisj2fi  32720  constr01  33732  bnj906  34920  bnj1137  34985  bnj1408  35026  cvmliftlem10  35281  cvmliftlem13  35283  sstotbnd2  37768  mapdrvallem3  41640  onsucunifi  43359  fvmptiunrelexplb0d  43673  fvmptiunrelexplb1d  43675  corclrcl  43696  trclrelexplem  43700  corcltrcl  43728  cotrclrcl  43731  iunincfi  45088  iundjiunlem  46457  meaiuninc3v  46482  caratheodorylem1  46524  ovnhoilem1  46599