MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssiun2s Structured version   Visualization version   GIF version

Theorem ssiun2s 4717
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
StepHypRef Expression
1 nfcv 2903 . 2 𝑥𝐶
2 nfcv 2903 . . 3 𝑥𝐷
3 nfiu1 4703 . . 3 𝑥 𝑥𝐴 𝐵
42, 3nfss 3738 . 2 𝑥 𝐷 𝑥𝐴 𝐵
5 ssiun2s.1 . . 3 (𝑥 = 𝐶𝐵 = 𝐷)
65sseq1d 3774 . 2 (𝑥 = 𝐶 → (𝐵 𝑥𝐴 𝐵𝐷 𝑥𝐴 𝐵))
7 ssiun2 4716 . 2 (𝑥𝐴𝐵 𝑥𝐴 𝐵)
81, 4, 6, 7vtoclgaf 3412 1 (𝐶𝐴𝐷 𝑥𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2140  wss 3716   ciun 4673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-v 3343  df-in 3723  df-ss 3730  df-iun 4675
This theorem is referenced by:  onfununi  7609  oaordi  7798  omordi  7818  dffi3  8505  alephordi  9108  domtriomlem  9477  pwxpndom2  9700  wunex2  9773  imasaddvallem  16412  imasvscaval  16421  iundisj2  23538  voliunlem1  23539  volsup  23545  iundisj2fi  29887  bnj906  31329  bnj1137  31392  bnj1408  31433  cvmliftlem10  31605  cvmliftlem13  31607  sstotbnd2  33905  mapdrvallem3  37456  fvmptiunrelexplb0d  38497  fvmptiunrelexplb1d  38499  corclrcl  38520  trclrelexplem  38524  corcltrcl  38552  cotrclrcl  38555  iunincfi  39790  iundjiunlem  41198  meaiuninc3v  41223  caratheodorylem1  41265  ovnhoilem1  41340
  Copyright terms: Public domain W3C validator