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

Theorem unissi 4916
Description: Subclass relationship for subclass union. Inference form of uniss 4915. (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 4915 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2ax-mp 5 1 𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3951   cuni 4907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908
This theorem is referenced by:  unidif  4942  unixpss  5820  riotassuni  7428  unifpw  9395  fiuni  9468  rankuni  9903  fin23lem29  10381  fin23lem30  10382  fin1a2lem12  10451  prdsds  17509  psss  18625  tgval2  22963  eltg4i  22967  ntrss2  23065  isopn3  23074  mretopd  23100  ordtbas  23200  cmpcov2  23398  tgcmp  23409  comppfsc  23540  alexsublem  24052  alexsubALTlem3  24057  alexsubALTlem4  24058  cldsubg  24119  bndth  24990  uniioombllem4  25621  uniioombllem5  25622  omssubadd  34302  cvmscld  35278  fnessref  36358  inunissunidif  37376  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  mbfresfi  37673  cover2  37722  salexct  46349  salgencntex  46358
  Copyright terms: Public domain W3C validator