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

Theorem unissd 4040
Description: Subclass relationship for subclass union. Deduction form of uniss 4037. (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 4037 . 2  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
31, 2syl 16 1  |-  ( ph  ->  U. A  C_  U. B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3321   U.cuni 4016
This theorem is referenced by:  dffv2  5797  onfununi  6604  fiuni  7434  dfac2a  8011  incexc  12618  incexc2  12619  isacs1i  13883  isacs3lem  14593  acsmapd  14605  acsmap2d  14606  dprd2da  15601  eltg3i  17027  unitg  17033  tgss  17034  tgcmp  17465  cmpfi  17472  alexsubALTlem4  18082  ptcmplem3  18086  ustbas2  18256  uniioombllem3  19478  shsupunss  22849  dya2iocucvr  24635  cvmscld  24961  nofulllem3  25660  onsucsuccmpi  26194  fnemeet1  26396  fnejoin1  26398  heibor1  26520  heiborlem10  26530  hbt  27312
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-in 3328  df-ss 3335  df-uni 4017
  Copyright terms: Public domain W3C validator