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

Theorem iunss1 4724
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 3864 . . 3 (𝐴𝐵 → (∃𝑥𝐴 𝑦𝐶 → ∃𝑥𝐵 𝑦𝐶))
2 eliun 4716 . . 3 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
3 eliun 4716 . . 3 (𝑦 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝑦𝐶)
41, 2, 33imtr4g 287 . 2 (𝐴𝐵 → (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
54ssrdv 3804 1 (𝐴𝐵 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  wrex 3097  wss 3769   ciun 4712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-v 3393  df-in 3776  df-ss 3783  df-iun 4714
This theorem is referenced by:  iuneq1  4726  iunxdif2  4760  oelim2  7912  fsumiun  14775  ovolfiniun  23482  uniioovol  23560  fusgreghash2wspv  27510  esum2dlem  30479  esum2d  30480  carsgclctunlem2  30706  bnj1413  31426  bnj1408  31427  volsupnfl  33767  corclrcl  38499  cotrcltrcl  38517  iuneqfzuzlem  40030  fsumiunss  40287  sge0iunmptlemfi  41109  sge0iunmptlemre  41111  carageniuncllem1  41217  carageniuncllem2  41218  caratheodorylem2  41223  ovnsubaddlem1  41266
  Copyright terms: Public domain W3C validator