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

Theorem unissi 4231
Description: Subclass relationship for subclass union. Inference form of uniss 4229. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
unissi.1
Assertion
Ref Expression
unissi

Proof of Theorem unissi
StepHypRef Expression
1 unissi.1 . 2
2 uniss 4229 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  C_wss 3442  U.cuni 4208
This theorem is referenced by:  unidif  4242  unixpss  5072  riotassuniOLD  6220  unifpw  7749  fiuni  7814  rankuni  8207  fin23lem29  8647  fin23lem30  8648  fin1a2lem12  8717  prdsds  14561  psss  15543  tgval2  18960  eltg4i  18964  unitg  18971  ntrss2  19060  isopn3  19069  mretopd  19095  ordtbas  19195  cmpcov2  19392  tgcmp  19403  alexsublem  20015  alexsubALTlem3  20020  alexsubALTlem4  20021  cldsubg  20080  bndth  20929  uniioombllem4  21466  uniioombllem5  21467  cvmscld  27618  mblfinlem3  28890  mblfinlem4  28891  ismblfin  28892  mbfresfi  28898  fnessref  29025  comppfsc  29039  cover2  29067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083  df-in 3449  df-ss 3456  df-uni 4209
  Copyright terms: Public domain W3C validator