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

Theorem uniss 3789
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 3116 . . . . 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 3771 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 3771 . . 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 3127 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 3094   U.cuni 3768
This theorem is referenced by:  unissi  3791  unissd  3792  unidif  3800  intssuni2  3828  uniintsn  3840  unixpss  4752  relfld  5150  dffv2  5491  riotassuni  6276  onfununi  6291  unifpw  7091  fiuni  7114  trcl  7343  rankuni  7468  dfac2a  7689  cflm  7809  coflim  7820  cfslbn  7826  fin23lem29  7900  fin23lem30  7901  fin23lem41  7911  fin1a2lem12  7970  tskuni  8338  prdsval  13282  prdsbas  13284  prdsplusg  13285  prdsmulr  13286  prdsvsca  13287  prdsds  13290  prdshom  13293  mrcssv  13443  isacs1i  13486  catcfuccl  13868  catcxpccl  13908  isacs3lem  14196  mrelatlub  14216  mreclat  14217  psss  14250  dprdres  15190  dprd2da  15204  dmdprdsplit2lem  15207  tgval2  16621  eltg4i  16625  eltg3i  16626  unitg  16632  tgss  16633  tgcl  16634  distop  16660  fctop  16668  cctop  16670  ntrss2  16721  isopn3  16730  mretopd  16756  ordtbas  16849  cmpcov2  17044  tgcmp  17055  cmpcld  17056  uncmp  17057  cmpfi  17062  kgentopon  17160  txcmplem2  17263  filcon  17505  alexsublem  17665  alexsubALTlem3  17670  alexsubALTlem4  17671  alexsubALT  17672  ptcmplem3  17675  cldsubg  17720  bndth  18383  uniioombllem3  18867  uniioombllem4  18868  uniioombllem5  18869  dyadmbllem  18881  shsupcl  21842  hsupss  21845  shsupunss  21850  shatomistici  22866  cvmscld  23141  cvmliftlem15  23166  frrlem5c  23621  onsucsuccmpi  24222  uuniin  24418  inttrp  24439  inposet  24610  intfmu2  24851  bwt2  24924  tartarmap  25220  fnessref  25625  comppfsc  25639  fnemeet1  25647  fnejoin1  25649  filnetlem3  25661  cover2  25690  heibor1  25866  heiborlem1  25867  heiborlem10  25876  hbt  26666  lssats  28332  lpssat  28333  lssatle  28335  lssat  28336  dicval  30496
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108  df-uni 3769
  Copyright terms: Public domain W3C validator