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

Theorem iunss1 5006
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 4053 . . 3 (𝐴𝐵 → (∃𝑥𝐴 𝑦𝐶 → ∃𝑥𝐵 𝑦𝐶))
2 eliun 4995 . . 3 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
3 eliun 4995 . . 3 (𝑦 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝑦𝐶)
41, 2, 33imtr4g 296 . 2 (𝐴𝐵 → (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
54ssrdv 3989 1 (𝐴𝐵 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  wrex 3070  wss 3951   ciun 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-v 3482  df-ss 3968  df-iun 4993
This theorem is referenced by:  iuneq1  5008  iunxdif2  5053  oelim2  8633  fsumiun  15857  ovolfiniun  25536  uniioovol  25614  fusgreghash2wspv  30354  ssdifidllem  33484  esum2dlem  34093  esum2d  34094  carsgclctunlem2  34321  bnj1413  35049  bnj1408  35050  volsupnfl  37672  corclrcl  43720  cotrcltrcl  43738  iuneqfzuzlem  45345  fsumiunss  45590  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  carageniuncllem1  46536  carageniuncllem2  46537  caratheodorylem2  46542  ovnsubaddlem1  46585
  Copyright terms: Public domain W3C validator