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

Theorem unissi 4613
Description: Subclass relationship for subclass union. Inference form of uniss 4610. (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 4610 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2ax-mp 5 1 𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3715   cuni 4588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729  df-uni 4589
This theorem is referenced by:  unidif  4623  unixpss  5390  riotassuni  6811  unifpw  8434  fiuni  8499  rankuni  8899  fin23lem29  9355  fin23lem30  9356  fin1a2lem12  9425  prdsds  16326  psss  17415  tgval2  20962  eltg4i  20966  ntrss2  21063  isopn3  21072  mretopd  21098  ordtbas  21198  cmpcov2  21395  tgcmp  21406  comppfsc  21537  alexsublem  22049  alexsubALTlem3  22054  alexsubALTlem4  22055  cldsubg  22115  bndth  22958  uniioombllem4  23554  uniioombllem5  23555  omssubadd  30671  cvmscld  31562  fnessref  32658  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  mbfresfi  33769  cover2  33821  salexct  41055  salgencntex  41064
  Copyright terms: Public domain W3C validator