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

Theorem ss2iun 4527
 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 3589 . . . . 5 (𝐵𝐶 → (𝑦𝐵𝑦𝐶))
21ralimi 2949 . . . 4 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴 (𝑦𝐵𝑦𝐶))
3 rexim 3005 . . . 4 (∀𝑥𝐴 (𝑦𝐵𝑦𝐶) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
42, 3syl 17 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦𝐶))
5 eliun 4515 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
6 eliun 4515 . . 3 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
74, 5, 63imtr4g 285 . 2 (∀𝑥𝐴 𝐵𝐶 → (𝑦 𝑥𝐴 𝐵𝑦 𝑥𝐴 𝐶))
87ssrdv 3601 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 𝑥𝐴 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1988  ∀wral 2909  ∃wrex 2910   ⊆ wss 3567  ∪ ciun 4511 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-v 3197  df-in 3574  df-ss 3581  df-iun 4513 This theorem is referenced by:  iuneq2  4528  abnexg  6949  oawordri  7615  omwordri  7637  oewordri  7657  oeworde  7658  r1val1  8634  cfslb2n  9075  imasaddvallem  16170  dprdss  18409  tgcmp  21185  txcmplem1  21425  txcmplem2  21426  xkococnlem  21443  alexsubALT  21836  ptcmplem3  21839  metnrmlem2  22644  uniiccvol  23329  dvfval  23642  bnj1145  31035  bnj1136  31039  filnetlem3  32350  poimirlem32  33412  sstotbnd2  33544  equivtotbnd  33548  trclrelexplem  37822  corcltrcl  37850  cotrclrcl  37853  ovolval5lem2  40630  ovolval5lem3  40631  smflimsuplem7  40795
 Copyright terms: Public domain W3C validator