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

Theorem ss2iun 4971
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 3936 . . . . 5 (𝐵𝐶 → (𝑦𝐵𝑦𝐶))
21ralimi 3085 . . . 4 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴 (𝑦𝐵𝑦𝐶))
3 rexim 3089 . . . 4 (∀𝑥𝐴 (𝑦𝐵𝑦𝐶) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
42, 3syl 17 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
5 eliun 4957 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
6 eliun 4957 . . 3 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
74, 5, 63imtr4g 295 . 2 (∀𝑥𝐴 𝐵𝐶 → (𝑦 𝑥𝐴 𝐵𝑦 𝑥𝐴 𝐶))
87ssrdv 3949 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wral 3063  wrex 3072  wss 3909   ciun 4953
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3064  df-rex 3073  df-v 3446  df-in 3916  df-ss 3926  df-iun 4955
This theorem is referenced by:  iuneq2  4972  abnexg  7687  oawordri  8494  omwordri  8516  oewordri  8536  oeworde  8537  r1val1  9719  cfslb2n  10201  imasaddvallem  17408  dprdss  19804  tgcmp  22748  txcmplem1  22988  txcmplem2  22989  xkococnlem  23006  alexsubALT  23398  ptcmplem3  23401  metnrmlem2  24219  uniiccvol  24940  dvfval  25257  gsumpart  31792  bnj1145  33496  bnj1136  33500  filnetlem3  34841  poimirlem32  36099  sstotbnd2  36222  equivtotbnd  36226  trclrelexplem  41963  corcltrcl  41991  cotrclrcl  41994  ovolval5lem2  44864  ovolval5lem3  44865  smflimsuplem7  45037
  Copyright terms: Public domain W3C validator