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

Theorem uniss 4252
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 3481 . . . . 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 1695 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 4234 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 4234 . . 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 3493 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1597    e. wcel 1802    C_ wss 3459   U.cuni 4231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3466  df-ss 3473  df-uni 4232
This theorem is referenced by:  unissi  4254  unissd  4255  intssuni2  4294  uniintsn  4306  relfld  5520  dffv2  5928  trcl  8159  cflm  8630  coflim  8641  cfslbn  8647  fin23lem41  8732  fin1a2lem12  8791  tskuni  9161  prdsval  14726  prdsbas  14728  prdsplusg  14729  prdsmulr  14730  prdsvsca  14731  prdshom  14738  mrcssv  14885  catcfuccl  15307  catcxpccl  15347  mrelatlub  15687  mreclatBAD  15688  dprdres  16946  dmdprdsplit2lem  16965  tgcl  19341  distop  19367  fctop  19375  cctop  19377  neiptoptop  19502  cmpcld  19772  uncmp  19773  cmpfi  19778  bwthOLD  19781  comppfsc  19903  kgentopon  19909  txcmplem2  20013  filcon  20254  alexsubALTlem3  20419  alexsubALT  20421  ptcmplem3  20424  dyadmbllem  21878  shsupcl  26125  hsupss  26128  shatomistici  27149  cvmliftlem15  28613  frrlem5c  29365  filnetlem3  30170  heiborlem1  30279  lssats  34460  lpssat  34461  lssatle  34463  lssat  34464  dicval  36626
  Copyright terms: Public domain W3C validator