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

Theorem unissi 4235
Description: Subclass relationship for subclass union. Inference form of uniss 4233. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
unissi.1  |-  A  C_  B
Assertion
Ref Expression
unissi  |-  U. A  C_ 
U. B

Proof of Theorem unissi
StepHypRef Expression
1 unissi.1 . 2  |-  A  C_  B
2 uniss 4233 . 2  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
31, 2ax-mp 5 1  |-  U. A  C_ 
U. B
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3416   U.cuni 4212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430  df-uni 4213
This theorem is referenced by:  unidif  4245  unixpss  4971  riotassuni  6318  unifpw  7908  fiuni  7973  rankuni  8365  fin23lem29  8802  fin23lem30  8803  fin1a2lem12  8872  prdsds  15417  psss  16515  tgval2  20026  eltg4i  20030  unitgOLD  20038  ntrss2  20127  isopn3  20137  mretopd  20163  ordtbas  20263  cmpcov2  20460  tgcmp  20471  comppfsc  20602  alexsublem  21114  alexsubALTlem3  21119  alexsubALTlem4  21120  cldsubg  21180  bndth  22041  uniioombllem4  22600  uniioombllem5  22601  omssubadd  29178  omssubaddOLD  29182  cvmscld  30046  fnessref  31063  mblfinlem3  32025  mblfinlem4  32026  ismblfin  32027  mbfresfi  32033  cover2  32086  salexct  38294  salgencntex  38303
  Copyright terms: Public domain W3C validator