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

Theorem uniss 3748
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
StepHypRef Expression
1 ssel 3097 . . . . 5  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
21anim2d 550 . . . 4  |-  ( A 
C_  B  ->  (
( x  e.  y  /\  y  e.  A
)  ->  ( x  e.  y  /\  y  e.  B ) ) )
32eximdv 2018 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 3730 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 3730 . . 3  |-  ( x  e.  U. B  <->  E. y
( x  e.  y  /\  y  e.  B
) )
63, 4, 53imtr4g 263 . 2  |-  ( A 
C_  B  ->  (
x  e.  U. A  ->  x  e.  U. B
) )
76ssrdv 3106 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   E.wex 1537    e. wcel 1621    C_ wss 3078   U.cuni 3727
This theorem is referenced by:  unidif  3757  intssuni2  3785  uniintsn  3797  unixpss  4706  relfld  5104  dffv2  5444  riotassuni  6229  onfununi  6244  unifpw  7042  fiuni  7065  trcl  7294  rankuni  7419  dfac2a  7640  cflm  7760  coflim  7771  cfslbn  7777  fin23lem29  7851  fin23lem30  7852  fin23lem41  7862  fin1a2lem12  7921  tskuni  8285  prdsval  13229  prdsbas  13231  prdsplusg  13232  prdsmulr  13233  prdsvsca  13234  prdsds  13237  prdshom  13240  mrcssv  13388  isacs1i  13403  catcfuccl  13785  catcxpccl  13825  isacs3lem  14113  mrelatlub  14124  mreclat  14125  psss  14158  dprdres  15098  dprd2da  15112  dmdprdsplit2lem  15115  tgval2  16526  eltg4i  16530  eltg3i  16531  unitg  16537  tgss  16538  tgcl  16539  distop  16565  fctop  16573  cctop  16575  ntrss2  16626  isopn3  16635  mretopd  16661  ordtbas  16754  cmpcov2  16949  tgcmp  16960  cmpcld  16961  uncmp  16962  cmpfi  16967  kgentopon  17065  txcmplem2  17168  filcon  17410  alexsublem  17570  alexsubALTlem3  17575  alexsubALTlem4  17576  alexsubALT  17577  ptcmplem3  17580  cldsubg  17625  bndth  18288  uniioombllem3  18772  uniioombllem4  18773  uniioombllem5  18774  dyadmbllem  18786  shsupcl  21747  hsupss  21750  shsupunss  21755  shatomistici  22771  cvmscld  22975  cvmliftlem15  23000  frrlem5c  23455  onsucsuccmpi  24056  uuniin  24252  inttrp  24273  inposet  24444  intfmu2  24685  bwt2  24758  tartarmap  25054  fnessref  25459  comppfsc  25473  fnemeet1  25481  fnejoin1  25483  filnetlem3  25495  cover2  25524  heibor1  25700  heiborlem1  25701  heiborlem10  25710  hbt  26500  lssats  27891  lpssat  27892  lssatle  27894  lssat  27895  dicval  30055
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089  df-uni 3728
  Copyright terms: Public domain W3C validator