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

Theorem iunss1 5012
Description: Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
iunss1 (𝐴𝐵 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem iunss1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ssrexv 4052 . . 3 (𝐴𝐵 → (∃𝑥𝐴 𝑦𝐶 → ∃𝑥𝐵 𝑦𝐶))
2 eliun 5002 . . 3 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
3 eliun 5002 . . 3 (𝑦 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝑦𝐶)
41, 2, 33imtr4g 296 . 2 (𝐴𝐵 → (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
54ssrdv 3989 1 (𝐴𝐵 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wrex 3071  wss 3949   ciun 4998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-v 3477  df-in 3956  df-ss 3966  df-iun 5000
This theorem is referenced by:  iuneq1  5014  iunxdif2  5057  oelim2  8595  fsumiun  15767  ovolfiniun  25018  uniioovol  25096  fusgreghash2wspv  29619  esum2dlem  33121  esum2d  33122  carsgclctunlem2  33349  bnj1413  34077  bnj1408  34078  volsupnfl  36581  corclrcl  42506  cotrcltrcl  42524  iuneqfzuzlem  44092  fsumiunss  44339  sge0iunmptlemfi  45177  sge0iunmptlemre  45179  carageniuncllem1  45285  carageniuncllem2  45286  caratheodorylem2  45291  ovnsubaddlem1  45334
  Copyright terms: Public domain W3C validator