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

Theorem ss2iun 4769
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 3815 . . . . 5 (𝐵𝐶 → (𝑦𝐵𝑦𝐶))
21ralimi 3134 . . . 4 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴 (𝑦𝐵𝑦𝐶))
3 rexim 3189 . . . 4 (∀𝑥𝐴 (𝑦𝐵𝑦𝐶) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
42, 3syl 17 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
5 eliun 4757 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
6 eliun 4757 . . 3 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
74, 5, 63imtr4g 288 . 2 (∀𝑥𝐴 𝐵𝐶 → (𝑦 𝑥𝐴 𝐵𝑦 𝑥𝐴 𝐶))
87ssrdv 3827 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wral 3090  wrex 3091  wss 3792   ciun 4753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-v 3400  df-in 3799  df-ss 3806  df-iun 4755
This theorem is referenced by:  iuneq2  4770  abnexg  7242  oawordri  7914  omwordri  7936  oewordri  7956  oeworde  7957  r1val1  8946  cfslb2n  9425  imasaddvallem  16575  dprdss  18815  tgcmp  21613  txcmplem1  21853  txcmplem2  21854  xkococnlem  21871  alexsubALT  22263  ptcmplem3  22266  metnrmlem2  23071  uniiccvol  23784  dvfval  24098  bnj1145  31660  bnj1136  31664  filnetlem3  32963  poimirlem32  34069  sstotbnd2  34199  equivtotbnd  34203  trclrelexplem  38964  corcltrcl  38992  cotrclrcl  38995  ovolval5lem2  41798  ovolval5lem3  41799  smflimsuplem7  41963
  Copyright terms: Public domain W3C validator