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

Theorem ss2iun 5014
Description: Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
ss2iun (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 𝑥𝐴 𝐶)

Proof of Theorem ss2iun
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ssel 3988 . . . . 5 (𝐵𝐶 → (𝑦𝐵𝑦𝐶))
21ralimi 3080 . . . 4 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴 (𝑦𝐵𝑦𝐶))
3 rexim 3084 . . . 4 (∀𝑥𝐴 (𝑦𝐵𝑦𝐶) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
42, 3syl 17 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
5 eliun 4999 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
6 eliun 4999 . . 3 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
74, 5, 63imtr4g 296 . 2 (∀𝑥𝐴 𝐵𝐶 → (𝑦 𝑥𝐴 𝐵𝑦 𝑥𝐴 𝐶))
87ssrdv 4000 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wral 3058  wrex 3067  wss 3962   ciun 4995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-v 3479  df-ss 3979  df-iun 4997
This theorem is referenced by:  iuneq2  5015  abnexg  7774  oawordri  8586  omwordri  8608  oewordri  8628  oeworde  8629  r1val1  9823  cfslb2n  10305  imasaddvallem  17575  dprdss  20063  tgcmp  23424  txcmplem1  23664  txcmplem2  23665  xkococnlem  23682  alexsubALT  24074  ptcmplem3  24077  metnrmlem2  24895  uniiccvol  25628  dvfval  25946  gsumpart  33042  bnj1145  34985  bnj1136  34989  filnetlem3  36362  poimirlem32  37638  sstotbnd2  37760  equivtotbnd  37764  trclrelexplem  43700  corcltrcl  43728  cotrclrcl  43731  ovolval5lem2  46608  ovolval5lem3  46609  smflimsuplem7  46781
  Copyright terms: Public domain W3C validator