Theorem ssiun2s 4934

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ⊆ wss 3843  ∪ ciun 4881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rex 3059  df-v 3400  df-in 3850  df-ss 3860  df-iun 4883

This theorem is referenced by:  fviunfun  7671  onfununi  8007  oaordi  8203  omordi  8223  dffi3  8968  alephordi  9574  domtriomlem  9942  pwxpndom2  10165  wunex2  10238  imasaddvallem  16905  imasvscaval  16914  iundisj2  24301  voliunlem1  24302  volsup  24308  iundisj2fi  30693  bnj906  32481  bnj1137  32546  bnj1408  32587  cvmliftlem10  32827  cvmliftlem13  32829  sstotbnd2  35555  mapdrvallem3  39283  fvmptiunrelexplb0d  40838  fvmptiunrelexplb1d  40840  corclrcl  40861  trclrelexplem  40865  corcltrcl  40893  cotrclrcl  40896  iunincfi  42182  iundjiunlem  43539  meaiuninc3v  43564  caratheodorylem1  43606  ovnhoilem1  43681