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

Theorem uniss 3822
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 3149 . . . . 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 2019 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 3804 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 3804 . . 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 3160 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 3127   U.cuni 3801
This theorem is referenced by:  unissi  3824  unissd  3825  unidif  3833  intssuni2  3861  uniintsn  3873  unixpss  4787  relfld  5185  dffv2  5526  riotassuni  6311  onfununi  6326  unifpw  7126  fiuni  7149  trcl  7378  rankuni  7503  dfac2a  7724  cflm  7844  coflim  7855  cfslbn  7861  fin23lem29  7935  fin23lem30  7936  fin23lem41  7946  fin1a2lem12  8005  tskuni  8373  prdsval  13317  prdsbas  13319  prdsplusg  13320  prdsmulr  13321  prdsvsca  13322  prdsds  13325  prdshom  13328  mrcssv  13478  isacs1i  13521  catcfuccl  13903  catcxpccl  13943  isacs3lem  14231  mrelatlub  14251  mreclat  14252  psss  14285  dprdres  15225  dprd2da  15239  dmdprdsplit2lem  15242  tgval2  16656  eltg4i  16660  eltg3i  16661  unitg  16667  tgss  16668  tgcl  16669  distop  16695  fctop  16703  cctop  16705  ntrss2  16756  isopn3  16765  mretopd  16791  ordtbas  16884  cmpcov2  17079  tgcmp  17090  cmpcld  17091  uncmp  17092  cmpfi  17097  kgentopon  17195  txcmplem2  17298  filcon  17540  alexsublem  17700  alexsubALTlem3  17705  alexsubALTlem4  17706  alexsubALT  17707  ptcmplem3  17710  cldsubg  17755  bndth  18418  uniioombllem3  18902  uniioombllem4  18903  uniioombllem5  18904  dyadmbllem  18916  shsupcl  21877  hsupss  21880  shsupunss  21885  shatomistici  22901  cvmscld  23176  cvmliftlem15  23201  frrlem5c  23656  onsucsuccmpi  24257  uuniin  24453  inttrp  24474  inposet  24645  intfmu2  24886  bwt2  24959  tartarmap  25255  fnessref  25660  comppfsc  25674  fnemeet1  25682  fnejoin1  25684  filnetlem3  25696  cover2  25725  heibor1  25901  heiborlem1  25902  heiborlem10  25911  hbt  26701  lssats  28369  lpssat  28370  lssatle  28372  lssat  28373  dicval  30533
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 1927  ax-ext 2239
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141  df-uni 3802
  Copyright terms: Public domain W3C validator