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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900  ∪ ciun 4956

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-v 3456  df-ss 3901  df-iun 4958

This theorem is used by:  fviunfun  7991  onfununi  8387  oaordi  8592  omordi  8612  dffi3  9460  alephordi  10192  domtriomlem  10559  pwxpndom2  10789  wunex2  10862  imasaddvallem  17751  imasvscaval  17760  iundisj2  25925  voliunlem1  25926  volsup  25932  iundisj2fi  33485  constr01  34485  bnj906  35671  bnj1137  35736  bnj1408  35777  ptpconn  36206  cvmliftlem10  36267  cvmliftlem13  36269  ttciunun  37514  sstotbnd2  38974  mapdrvallem3  42969  onsucunifi  44633  fvmptiunrelexplb0d  44945  fvmptiunrelexplb1d  44947  corclrcl  44968  trclrelexplem  44972  corcltrcl  45000  cotrclrcl  45003  iunincfi  46382  iundjiunlem  47742  meaiuninc3v  47767  caratheodorylem1  47809  ovnhoilem1  47884