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

Theorem ss2iun 5011
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 3972 . . . . 5 (𝐵𝐶 → (𝑦𝐵𝑦𝐶))
21ralimi 3073 . . . 4 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴 (𝑦𝐵𝑦𝐶))
3 rexim 3077 . . . 4 (∀𝑥𝐴 (𝑦𝐵𝑦𝐶) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
42, 3syl 17 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
5 eliun 4997 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
6 eliun 4997 . . 3 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
74, 5, 63imtr4g 295 . 2 (∀𝑥𝐴 𝐵𝐶 → (𝑦 𝑥𝐴 𝐵𝑦 𝑥𝐴 𝐶))
87ssrdv 3984 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2099  wral 3051  wrex 3060  wss 3946   ciun 4993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-v 3464  df-ss 3963  df-iun 4995
This theorem is referenced by:  iuneq2  5012  abnexg  7756  oawordri  8572  omwordri  8594  oewordri  8614  oeworde  8615  r1val1  9822  cfslb2n  10302  imasaddvallem  17539  dprdss  20025  tgcmp  23393  txcmplem1  23633  txcmplem2  23634  xkococnlem  23651  alexsubALT  24043  ptcmplem3  24046  metnrmlem2  24864  uniiccvol  25597  dvfval  25914  gsumpart  32927  bnj1145  34851  bnj1136  34855  filnetlem3  36105  poimirlem32  37366  sstotbnd2  37488  equivtotbnd  37492  trclrelexplem  43415  corcltrcl  43443  cotrclrcl  43446  ovolval5lem2  46310  ovolval5lem3  46311  smflimsuplem7  46483
  Copyright terms: Public domain W3C validator