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

Theorem uniss 4237
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 3458 . . . . 5  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
21anim2d 567 . . . 4  |-  ( A 
C_  B  ->  (
( x  e.  y  /\  y  e.  A
)  ->  ( x  e.  y  /\  y  e.  B ) ) )
32eximdv 1754 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 4219 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 4219 . . 3  |-  ( x  e.  U. B  <->  E. y
( x  e.  y  /\  y  e.  B
) )
63, 4, 53imtr4g 273 . 2  |-  ( A 
C_  B  ->  (
x  e.  U. A  ->  x  e.  U. B
) )
76ssrdv 3470 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   E.wex 1659    e. wcel 1868    C_ wss 3436   U.cuni 4216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-in 3443  df-ss 3450  df-uni 4217
This theorem is referenced by:  unissi  4239  unissd  4240  intssuni2  4278  uniintsn  4290  relfld  5377  dffv2  5951  trcl  8214  cflm  8681  coflim  8692  cfslbn  8698  fin23lem41  8783  fin1a2lem12  8842  tskuni  9209  prdsval  15341  prdsbas  15343  prdsplusg  15344  prdsmulr  15345  prdsvsca  15346  prdshom  15353  mrcssv  15508  catcfuccl  15992  catcxpccl  16080  mrelatlub  16420  mreclatBAD  16421  dprdres  17649  dmdprdsplit2lem  17666  tgcl  19972  distop  19998  fctop  20006  cctop  20008  neiptoptop  20134  cmpcld  20404  uncmp  20405  cmpfi  20410  comppfsc  20534  kgentopon  20540  txcmplem2  20644  filcon  20885  alexsubALTlem3  21051  alexsubALT  21053  ptcmplem3  21056  dyadmbllem  22544  shsupcl  26977  hsupss  26980  shatomistici  28000  pwuniss  28157  carsggect  29146  carsgclctun  29149  cvmliftlem15  30017  frrlem5c  30515  filnetlem3  31029  icoreunrn  31703  heiborlem1  32057  lssats  32497  lpssat  32498  lssatle  32500  lssat  32501  dicval  34663  pwsal  37977  prsal  37980  intsaluni  37989
  Copyright terms: Public domain W3C validator