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

Theorem unissi 4432
Description: Subclass relationship for subclass union. Inference form of uniss 4429. (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 4429 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2ax-mp 5 1 𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3559   cuni 4407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3191  df-in 3566  df-ss 3573  df-uni 4408
This theorem is referenced by:  unidif  4442  unixpss  5200  riotassuni  6608  unifpw  8221  fiuni  8286  rankuni  8678  fin23lem29  9115  fin23lem30  9116  fin1a2lem12  9185  prdsds  16056  psss  17146  tgval2  20684  eltg4i  20688  ntrss2  20784  isopn3  20793  mretopd  20819  ordtbas  20919  cmpcov2  21116  tgcmp  21127  comppfsc  21258  alexsublem  21771  alexsubALTlem3  21776  alexsubALTlem4  21777  cldsubg  21837  bndth  22680  uniioombllem4  23277  uniioombllem5  23278  omssubadd  30167  cvmscld  30998  fnessref  32029  mblfinlem3  33115  mblfinlem4  33116  ismblfin  33117  mbfresfi  33123  cover2  33175  salexct  39885  salgencntex  39894
  Copyright terms: Public domain W3C validator