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

Theorem unissd 4254
Description: Subclass relationship for subclass union. Deduction form of uniss 4251. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
unissd.1  |-  ( ph  ->  A  C_  B )
Assertion
Ref Expression
unissd  |-  ( ph  ->  U. A  C_  U. B
)

Proof of Theorem unissd
StepHypRef Expression
1 unissd.1 . 2  |-  ( ph  ->  A  C_  B )
2 uniss 4251 . 2  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
31, 2syl 16 1  |-  ( ph  ->  U. A  C_  U. B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3458   U.cuni 4230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465  df-ss 3472  df-uni 4231
This theorem is referenced by:  dffv2  5927  onfununi  7010  fiuni  7886  dfac2a  8508  incexc  13623  incexc2  13624  isacs1i  14926  isacs3lem  15665  acsmapd  15677  acsmap2d  15678  dprdres  16943  dprd2da  16959  eltg3i  19329  unitg  19335  tgss  19336  tgcmp  19767  cmpfi  19774  alexsubALTlem4  20416  ptcmplem3  20420  ustbas2  20594  uniioombllem3  21860  shsupunss  26129  locfinref  27710  cmpcref  27719  dya2iocucvr  28121  cvmscld  28584  nofulllem3  29432  onsucsuccmpi  29876  fnemeet1  30152  fnejoin1  30154  heibor1  30274  heiborlem10  30284  hbt  31047
  Copyright terms: Public domain W3C validator