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

Theorem unissi 4683
Description: Subclass relationship for subclass union. Inference form of uniss 4681. (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 4681 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2ax-mp 5 1 𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3798   cuni 4658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-ss 3812  df-uni 4659
This theorem is referenced by:  unidif  4693  unixpss  5468  riotassuni  6903  unifpw  8538  fiuni  8603  rankuni  9003  fin23lem29  9478  fin23lem30  9479  fin1a2lem12  9548  prdsds  16477  psss  17567  tgval2  21131  eltg4i  21135  ntrss2  21232  isopn3  21241  mretopd  21267  ordtbas  21367  cmpcov2  21564  tgcmp  21575  comppfsc  21706  alexsublem  22218  alexsubALTlem3  22223  alexsubALTlem4  22224  cldsubg  22284  bndth  23127  uniioombllem4  23752  uniioombllem5  23753  omssubadd  30907  cvmscld  31801  fnessref  32890  mblfinlem3  33992  mblfinlem4  33993  ismblfin  33994  mbfresfi  33999  cover2  34051  salexct  41343  salgencntex  41352
  Copyright terms: Public domain W3C validator