Theorem ssiun2s 5002

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 2896	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2896	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4980	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3924	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3963	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 5001	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3529	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ⊆ wss 3899  ∪ ciun 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059  df-v 3440  df-ss 3916  df-iun 4946

This theorem is referenced by:  fviunfun  7887  onfununi  8271  oaordi  8471  omordi  8491  dffi3  9332  alephordi  9982  domtriomlem  10350  pwxpndom2  10574  wunex2  10647  imasaddvallem  17448  imasvscaval  17457  iundisj2  25504  voliunlem1  25505  volsup  25511  iundisj2fi  32826  constr01  33848  bnj906  35035  bnj1137  35100  bnj1408  35141  cvmliftlem10  35437  cvmliftlem13  35439  sstotbnd2  37914  mapdrvallem3  41845  onsucunifi  43554  fvmptiunrelexplb0d  43867  fvmptiunrelexplb1d  43869  corclrcl  43890  trclrelexplem  43894  corcltrcl  43922  cotrclrcl  43925  iunincfi  45280  iundjiunlem  46645  meaiuninc3v  46670  caratheodorylem1  46712  ovnhoilem1  46787