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

Theorem uniss 4213
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 3451 . . . . 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 1677 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 4195 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 4195 . . 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 3463 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1587    e. wcel 1758    C_ wss 3429   U.cuni 4192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-in 3436  df-ss 3443  df-uni 4193
This theorem is referenced by:  unissi  4215  unissd  4216  intssuni2  4254  uniintsn  4266  relfld  5464  dffv2  5866  trcl  8052  cflm  8523  coflim  8534  cfslbn  8540  fin23lem41  8625  fin1a2lem12  8684  tskuni  9054  prdsval  14504  prdsbas  14506  prdsplusg  14507  prdsmulr  14508  prdsvsca  14509  prdshom  14516  mrcssv  14663  catcfuccl  15088  catcxpccl  15128  mrelatlub  15467  mreclatBAD  15468  dprdres  16639  dmdprdsplit2lem  16658  tgcl  18699  distop  18725  fctop  18733  cctop  18735  neiptoptop  18860  cmpcld  19130  uncmp  19131  cmpfi  19136  bwthOLD  19139  kgentopon  19236  txcmplem2  19340  filcon  19581  alexsubALTlem3  19746  alexsubALT  19748  ptcmplem3  19751  dyadmbllem  21205  shsupcl  24886  hsupss  24889  shatomistici  25910  cvmliftlem15  27324  frrlem5c  27911  comppfsc  28720  filnetlem3  28742  heiborlem1  28851  lssats  32966  lpssat  32967  lssatle  32969  lssat  32970  dicval  35130
  Copyright terms: Public domain W3C validator