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

Theorem ssiun2s 4969
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 2982 . 2 𝑥𝐶
2 nfcv 2982 . . 3 𝑥𝐷
3 nfiu1 4950 . . 3 𝑥 𝑥𝐴 𝐵
42, 3nfss 3964 . 2 𝑥 𝐷 𝑥𝐴 𝐵
5 ssiun2s.1 . . 3 (𝑥 = 𝐶𝐵 = 𝐷)
65sseq1d 4002 . 2 (𝑥 = 𝐶 → (𝐵 𝑥𝐴 𝐵𝐷 𝑥𝐴 𝐵))
7 ssiun2 4968 . 2 (𝑥𝐴𝐵 𝑥𝐴 𝐵)
81, 4, 6, 7vtoclgaf 3578 1 (𝐶𝐴𝐷 𝑥𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  wss 3940   ciun 4917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-v 3502  df-in 3947  df-ss 3956  df-iun 4919
This theorem is referenced by:  fviunfun  7642  onfununi  7974  oaordi  8167  omordi  8187  dffi3  8889  alephordi  9494  domtriomlem  9858  pwxpndom2  10081  wunex2  10154  imasaddvallem  16797  imasvscaval  16806  iundisj2  24084  voliunlem1  24085  volsup  24091  iundisj2fi  30452  bnj906  32107  bnj1137  32170  bnj1408  32211  cvmliftlem10  32444  cvmliftlem13  32446  sstotbnd2  34939  mapdrvallem3  38668  fvmptiunrelexplb0d  39913  fvmptiunrelexplb1d  39915  corclrcl  39936  trclrelexplem  39940  corcltrcl  39968  cotrclrcl  39971  iunincfi  41244  iundjiunlem  42626  meaiuninc3v  42651  caratheodorylem1  42693  ovnhoilem1  42768
  Copyright terms: Public domain W3C validator