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 2922	. 2 ⊢ Ⅎ𝑥𝐶
2		nfcv 2922	. . 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 3535	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 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3916  df-iun 4953

This theorem is used by:  fviunfun  7943  onfununi  8331  oaordi  8536  omordi  8556  dffi3  9404  alephordi  10080  domtriomlem  10447  pwxpndom2  10677  wunex2  10750  imasaddvallem  17618  imasvscaval  17627  iundisj2  25780  voliunlem1  25781  volsup  25787  iundisj2fi  33271  constr01  34255  bnj906  35442  bnj1137  35507  bnj1408  35548  cvmliftlem10  35876  cvmliftlem13  35878  ttciunun  37133  sstotbnd2  38527  mapdrvallem3  42522  onsucunifi  44214  fvmptiunrelexplb0d  44527  fvmptiunrelexplb1d  44529  corclrcl  44550  trclrelexplem  44554  corcltrcl  44582  cotrclrcl  44585  iunincfi  45929  iundjiunlem  47290  meaiuninc3v  47315  caratheodorylem1  47357  ovnhoilem1  47432