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

Theorem uniss 4266
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 3498 . . . . 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 1686 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 4248 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 4248 . . 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 3510 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1596    e. wcel 1767    C_ wss 3476   U.cuni 4245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-uni 4246
This theorem is referenced by:  unissi  4268  unissd  4269  intssuni2  4307  uniintsn  4319  relfld  5531  dffv2  5938  trcl  8155  cflm  8626  coflim  8637  cfslbn  8643  fin23lem41  8728  fin1a2lem12  8787  tskuni  9157  prdsval  14706  prdsbas  14708  prdsplusg  14709  prdsmulr  14710  prdsvsca  14711  prdshom  14718  mrcssv  14865  catcfuccl  15290  catcxpccl  15330  mrelatlub  15669  mreclatBAD  15670  dprdres  16865  dmdprdsplit2lem  16884  tgcl  19237  distop  19263  fctop  19271  cctop  19273  neiptoptop  19398  cmpcld  19668  uncmp  19669  cmpfi  19674  bwthOLD  19677  kgentopon  19774  txcmplem2  19878  filcon  20119  alexsubALTlem3  20284  alexsubALT  20286  ptcmplem3  20289  dyadmbllem  21743  shsupcl  25932  hsupss  25935  shatomistici  26956  cvmliftlem15  28383  frrlem5c  28970  comppfsc  29779  filnetlem3  29801  heiborlem1  29910  lssats  33809  lpssat  33810  lssatle  33812  lssat  33813  dicval  35973
  Copyright terms: Public domain W3C validator