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

Theorem unissd 4103
Description: Subclass relationship for subclass union. Deduction form of uniss 4100. (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 4100 . 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 3316   U.cuni 4079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-uni 4080
This theorem is referenced by:  dffv2  5752  onfununi  6788  fiuni  7666  dfac2a  8287  incexc  13282  incexc2  13283  isacs1i  14577  isacs3lem  15318  acsmapd  15330  acsmap2d  15331  dprd2da  16514  eltg3i  18407  unitg  18413  tgss  18414  tgcmp  18845  cmpfi  18852  alexsubALTlem4  19463  ptcmplem3  19467  ustbas2  19641  uniioombllem3  20906  shsupunss  24571  dya2iocucvr  26552  cvmscld  27009  nofulllem3  27691  onsucsuccmpi  28136  fnemeet1  28428  fnejoin1  28430  heibor1  28550  heiborlem10  28560  hbt  29328
  Copyright terms: Public domain W3C validator