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

Theorem unissd 4259
Description: Subclass relationship for subclass union. Deduction form of uniss 4256. (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 4256 . 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 3461   U.cuni 4235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-ss 3475  df-uni 4236
This theorem is referenced by:  dffv2  5921  onfununi  7004  fiuni  7880  dfac2a  8501  incexc  13731  incexc2  13732  isacs1i  15146  isacs3lem  15995  acsmapd  16007  acsmap2d  16008  dprdres  17270  dprd2da  17286  eltg3i  19629  unitg  19635  unitgOLD  19636  tgss  19637  tgcmp  20068  cmpfi  20075  alexsubALTlem4  20716  ptcmplem3  20720  ustbas2  20894  uniioombllem3  22160  shsupunss  26462  locfinref  28079  cmpcref  28088  dya2iocucvr  28492  omssubadd  28508  carsggect  28526  cvmscld  28982  nofulllem3  29704  onsucsuccmpi  30136  fnemeet1  30424  fnejoin1  30426  heibor1  30546  heiborlem10  30556  hbt  31320
  Copyright terms: Public domain W3C validator