Theorem ssiun2s 5004

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 2898	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2898	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4982	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3926	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3965	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 5003	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3531	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

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

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 2184  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-v 3442  df-ss 3918  df-iun 4948

This theorem is referenced by:  fviunfun  7889  onfununi  8273  oaordi  8473  omordi  8493  dffi3  9334  alephordi  9984  domtriomlem  10352  pwxpndom2  10576  wunex2  10649  imasaddvallem  17450  imasvscaval  17459  iundisj2  25506  voliunlem1  25507  volsup  25513  iundisj2fi  32877  constr01  33899  bnj906  35086  bnj1137  35151  bnj1408  35192  cvmliftlem10  35488  cvmliftlem13  35490  sstotbnd2  37975  mapdrvallem3  41916  onsucunifi  43622  fvmptiunrelexplb0d  43935  fvmptiunrelexplb1d  43937  corclrcl  43958  trclrelexplem  43962  corcltrcl  43990  cotrclrcl  43993  iunincfi  45348  iundjiunlem  46713  meaiuninc3v  46738  caratheodorylem1  46780  ovnhoilem1  46855