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

Theorem unissi 4823
Description: Subclass relationship for subclass union. Inference form of uniss 4822. (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 4822 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2ax-mp 5 1 𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3913   cuni 4814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-v 3475  df-in 3920  df-ss 3930  df-uni 4815
This theorem is referenced by:  unidif  4848  unixpss  5659  riotassuni  7131  unifpw  8805  fiuni  8870  rankuni  9270  fin23lem29  9741  fin23lem30  9742  fin1a2lem12  9811  prdsds  16716  psss  17803  tgval2  21540  eltg4i  21544  ntrss2  21641  isopn3  21650  mretopd  21676  ordtbas  21776  cmpcov2  21974  tgcmp  21985  comppfsc  22116  alexsublem  22628  alexsubALTlem3  22633  alexsubALTlem4  22634  cldsubg  22695  bndth  23542  uniioombllem4  24169  uniioombllem5  24170  omssubadd  31566  cvmscld  32528  fnessref  33713  inunissunidif  34673  mblfinlem3  34972  mblfinlem4  34973  ismblfin  34974  mbfresfi  34979  cover2  35028  salexct  42765  salgencntex  42774
  Copyright terms: Public domain W3C validator