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

Theorem unissi 4918
Description: Subclass relationship for subclass union. Inference form of uniss 4917. (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 4917 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2ax-mp 5 1 𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3949   cuni 4909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910
This theorem is referenced by:  unidif  4947  unixpss  5811  riotassuni  7406  unifpw  9355  fiuni  9423  rankuni  9858  fin23lem29  10336  fin23lem30  10337  fin1a2lem12  10406  prdsds  17410  psss  18533  tgval2  22459  eltg4i  22463  ntrss2  22561  isopn3  22570  mretopd  22596  ordtbas  22696  cmpcov2  22894  tgcmp  22905  comppfsc  23036  alexsublem  23548  alexsubALTlem3  23553  alexsubALTlem4  23554  cldsubg  23615  bndth  24474  uniioombllem4  25103  uniioombllem5  25104  omssubadd  33299  cvmscld  34264  fnessref  35242  inunissunidif  36256  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  mbfresfi  36534  cover2  36583  salexct  45050  salgencntex  45059
  Copyright terms: Public domain W3C validator