Theorem ssiun2s 5007

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 2923	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2923	. . 3 ⊢ Ⅎ𝑥𝐷
3		nfiu1 4986	. . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4	2, 3	nfss 3924	. 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
5		ssiun2s.1	. . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)
6	5	sseq1d 3962	. 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵))
7		ssiun2 5006	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
8	1, 4, 6, 7	vtoclgaf 3536	1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899  ∪ ciun 4951

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-v 3453  df-ss 3916  df-iun 4953

This theorem is used by:  fviunfun  7957  onfununi  8349  oaordi  8554  omordi  8574  dffi3  9423  alephordi  10153  domtriomlem  10520  pwxpndom2  10750  wunex2  10823  imasaddvallem  17701  imasvscaval  17710  iundisj2  25870  voliunlem1  25871  volsup  25877  iundisj2fi  33389  constr01  34374  bnj906  35560  bnj1137  35625  bnj1408  35666  cvmliftlem10  36059  cvmliftlem13  36061  ttciunun  37299  sstotbnd2  38708  mapdrvallem3  42703  onsucunifi  44371  fvmptiunrelexplb0d  44683  fvmptiunrelexplb1d  44685  corclrcl  44706  trclrelexplem  44710  corcltrcl  44738  cotrclrcl  44741  iunincfi  46108  iundjiunlem  47468  meaiuninc3v  47493  caratheodorylem1  47535  ovnhoilem1  47610