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

Theorem unissd 4136
Description: Subclass relationship for subclass union. Deduction form of uniss 4133. (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 4133 . 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 3349   U.cuni 4112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356  df-ss 3363  df-uni 4113
This theorem is referenced by:  dffv2  5785  onfununi  6823  fiuni  7699  dfac2a  8320  incexc  13321  incexc2  13322  isacs1i  14616  isacs3lem  15357  acsmapd  15369  acsmap2d  15370  dprd2da  16563  eltg3i  18588  unitg  18594  tgss  18595  tgcmp  19026  cmpfi  19033  alexsubALTlem4  19644  ptcmplem3  19648  ustbas2  19822  uniioombllem3  21087  shsupunss  24771  dya2iocucvr  26721  cvmscld  27184  nofulllem3  27867  onsucsuccmpi  28311  fnemeet1  28613  fnejoin1  28615  heibor1  28735  heiborlem10  28745  hbt  29512
  Copyright terms: Public domain W3C validator