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

Theorem uniss 4219
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 3426 . . . . 5  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
21anim2d 569 . . . 4  |-  ( A 
C_  B  ->  (
( x  e.  y  /\  y  e.  A
)  ->  ( x  e.  y  /\  y  e.  B ) ) )
32eximdv 1764 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 4201 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 4201 . . 3  |-  ( x  e.  U. B  <->  E. y
( x  e.  y  /\  y  e.  B
) )
63, 4, 53imtr4g 274 . 2  |-  ( A 
C_  B  ->  (
x  e.  U. A  ->  x  e.  U. B
) )
76ssrdv 3438 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371   E.wex 1663    e. wcel 1887    C_ wss 3404   U.cuni 4198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411  df-ss 3418  df-uni 4199
This theorem is referenced by:  unissi  4221  unissd  4222  intssuni2  4260  uniintsn  4272  relfld  5361  dffv2  5938  trcl  8212  cflm  8680  coflim  8691  cfslbn  8697  fin23lem41  8782  fin1a2lem12  8841  tskuni  9208  prdsval  15353  prdsbas  15355  prdsplusg  15356  prdsmulr  15357  prdsvsca  15358  prdshom  15365  mrcssv  15520  catcfuccl  16004  catcxpccl  16092  mrelatlub  16432  mreclatBAD  16433  dprdres  17661  dmdprdsplit2lem  17678  tgcl  19985  distop  20011  fctop  20019  cctop  20021  neiptoptop  20147  cmpcld  20417  uncmp  20418  cmpfi  20423  comppfsc  20547  kgentopon  20553  txcmplem2  20657  filcon  20898  alexsubALTlem3  21064  alexsubALT  21066  ptcmplem3  21069  dyadmbllem  22557  shsupcl  26991  hsupss  26994  shatomistici  28014  pwuniss  28167  carsggect  29150  carsgclctun  29153  cvmliftlem15  30021  frrlem5c  30520  filnetlem3  31036  icoreunrn  31762  heiborlem1  32143  lssats  32578  lpssat  32579  lssatle  32581  lssat  32582  dicval  34744  pwsal  38176  prsal  38179  intsaluni  38188
  Copyright terms: Public domain W3C validator