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

Theorem uniss 4100
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 3338 . . . . 5  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
21anim2d 560 . . . 4  |-  ( A 
C_  B  ->  (
( x  e.  y  /\  y  e.  A
)  ->  ( x  e.  y  /\  y  e.  B ) ) )
32eximdv 1675 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 4082 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 4082 . . 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 3350 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1589    e. wcel 1755    C_ wss 3316   U.cuni 4079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-uni 4080
This theorem is referenced by:  unissi  4102  unissd  4103  intssuni2  4141  uniintsn  4153  relfld  5351  dffv2  5752  trcl  7936  cflm  8407  coflim  8418  cfslbn  8424  fin23lem41  8509  fin1a2lem12  8568  tskuni  8937  prdsval  14375  prdsbas  14377  prdsplusg  14378  prdsmulr  14379  prdsvsca  14380  prdshom  14387  mrcssv  14534  catcfuccl  14959  catcxpccl  14999  mrelatlub  15338  mreclatBAD  15339  dprdres  16498  dmdprdsplit2lem  16517  tgcl  18415  distop  18441  fctop  18449  cctop  18451  neiptoptop  18576  cmpcld  18846  uncmp  18847  cmpfi  18852  bwthOLD  18855  kgentopon  18952  txcmplem2  19056  filcon  19297  alexsubALTlem3  19462  alexsubALT  19464  ptcmplem3  19467  dyadmbllem  20920  shsupcl  24563  hsupss  24566  shatomistici  25587  cvmliftlem15  27034  frrlem5c  27620  comppfsc  28420  filnetlem3  28442  heiborlem1  28551  lssats  32227  lpssat  32228  lssatle  32230  lssat  32231  dicval  34391
  Copyright terms: Public domain W3C validator