Theorem ssiun2s 5015

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ⊆ wss 3906  ∪ ciun 4958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-v 3459  df-ss 3923  df-iun 4960

This theorem is used by:  fviunfun  7948  onfununi  8334  oaordi  8537  omordi  8557  dffi3  9398  alephordi  10074  domtriomlem  10441  pwxpndom2  10667  wunex2  10740  imasaddvallem  17607  imasvscaval  17616  iundisj2  25761  voliunlem1  25762  volsup  25768  iundisj2fi  33214  constr01  34198  bnj906  35385  bnj1137  35450  bnj1408  35491  cvmliftlem10  35825  cvmliftlem13  35827  ttciunun  37081  sstotbnd2  38485  mapdrvallem3  42480  onsucunifi  44157  fvmptiunrelexplb0d  44470  fvmptiunrelexplb1d  44472  corclrcl  44493  trclrelexplem  44497  corcltrcl  44525  cotrclrcl  44528  iunincfi  45872  iundjiunlem  47233  meaiuninc3v  47258  caratheodorylem1  47300  ovnhoilem1  47375