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

Theorem ss2iun 4686
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 3736 . . . . 5 (𝐵𝐶 → (𝑦𝐵𝑦𝐶))
21ralimi 3088 . . . 4 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴 (𝑦𝐵𝑦𝐶))
3 rexim 3144 . . . 4 (∀𝑥𝐴 (𝑦𝐵𝑦𝐶) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
42, 3syl 17 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
5 eliun 4674 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
6 eliun 4674 . . 3 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
74, 5, 63imtr4g 285 . 2 (∀𝑥𝐴 𝐵𝐶 → (𝑦 𝑥𝐴 𝐵𝑦 𝑥𝐴 𝐶))
87ssrdv 3748 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2137  wral 3048  wrex 3049  wss 3713   ciun 4670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rex 3054  df-v 3340  df-in 3720  df-ss 3727  df-iun 4672
This theorem is referenced by:  iuneq2  4687  abnexg  7127  oawordri  7797  omwordri  7819  oewordri  7839  oeworde  7840  r1val1  8820  cfslb2n  9280  imasaddvallem  16389  dprdss  18626  tgcmp  21404  txcmplem1  21644  txcmplem2  21645  xkococnlem  21662  alexsubALT  22054  ptcmplem3  22057  metnrmlem2  22862  uniiccvol  23546  dvfval  23858  bnj1145  31366  bnj1136  31370  filnetlem3  32679  poimirlem32  33752  sstotbnd2  33884  equivtotbnd  33888  trclrelexplem  38503  corcltrcl  38531  cotrclrcl  38534  ovolval5lem2  41371  ovolval5lem3  41372  smflimsuplem7  41536
  Copyright terms: Public domain W3C validator