MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniss Structured version   Unicode version

Theorem uniss 4107
Description: Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Assertion
Ref Expression
uniss  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )

Proof of Theorem uniss
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3345 . . . . 5  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
21anim2d 565 . . . 4  |-  ( A 
C_  B  ->  (
( x  e.  y  /\  y  e.  A
)  ->  ( x  e.  y  /\  y  e.  B ) ) )
32eximdv 1676 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 4089 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 4089 . . 3  |-  ( x  e.  U. B  <->  E. y
( x  e.  y  /\  y  e.  B
) )
63, 4, 53imtr4g 270 . 2  |-  ( A 
C_  B  ->  (
x  e.  U. A  ->  x  e.  U. B
) )
76ssrdv 3357 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1586    e. wcel 1756    C_ wss 3323   U.cuni 4086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337  df-uni 4087
This theorem is referenced by:  unissi  4109  unissd  4110  intssuni2  4148  uniintsn  4160  relfld  5358  dffv2  5759  trcl  7940  cflm  8411  coflim  8422  cfslbn  8428  fin23lem41  8513  fin1a2lem12  8572  tskuni  8942  prdsval  14385  prdsbas  14387  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  prdshom  14397  mrcssv  14544  catcfuccl  14969  catcxpccl  15009  mrelatlub  15348  mreclatBAD  15349  dprdres  16513  dmdprdsplit2lem  16532  tgcl  18549  distop  18575  fctop  18583  cctop  18585  neiptoptop  18710  cmpcld  18980  uncmp  18981  cmpfi  18986  bwthOLD  18989  kgentopon  19086  txcmplem2  19190  filcon  19431  alexsubALTlem3  19596  alexsubALT  19598  ptcmplem3  19601  dyadmbllem  21054  shsupcl  24692  hsupss  24695  shatomistici  25716  cvmliftlem15  27139  frrlem5c  27725  comppfsc  28532  filnetlem3  28554  heiborlem1  28663  lssats  32497  lpssat  32498  lssatle  32500  lssat  32501  dicval  34661
  Copyright terms: Public domain W3C validator