Theorem ssiun2s 4935

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 2955	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2955	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4915	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3907	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3946	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 4934	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3521	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   ⊆ wss 3881  ∪ ciun 4881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-in 3888  df-ss 3898  df-iun 4883

This theorem is referenced by:  fviunfun  7628  onfununi  7961  oaordi  8155  omordi  8175  dffi3  8879  alephordi  9485  domtriomlem  9853  pwxpndom2  10076  wunex2  10149  imasaddvallem  16794  imasvscaval  16803  iundisj2  24153  voliunlem1  24154  volsup  24160  iundisj2fi  30546  bnj906  32312  bnj1137  32377  bnj1408  32418  cvmliftlem10  32654  cvmliftlem13  32656  sstotbnd2  35212  mapdrvallem3  38942  fvmptiunrelexplb0d  40385  fvmptiunrelexplb1d  40387  corclrcl  40408  trclrelexplem  40412  corcltrcl  40440  cotrclrcl  40443  iunincfi  41730  iundjiunlem  43098  meaiuninc3v  43123  caratheodorylem1  43165  ovnhoilem1  43240