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

Theorem unissi 4242
Description: Subclass relationship for subclass union. Inference form of uniss 4240. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
unissi.1  |-  A  C_  B
Assertion
Ref Expression
unissi  |-  U. A  C_ 
U. B

Proof of Theorem unissi
StepHypRef Expression
1 unissi.1 . 2  |-  A  C_  B
2 uniss 4240 . 2  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
31, 2ax-mp 5 1  |-  U. A  C_ 
U. B
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3436   U.cuni 4219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-in 3443  df-ss 3450  df-uni 4220
This theorem is referenced by:  unidif  4252  unixpss  4968  riotassuni  6304  unifpw  7887  fiuni  7952  rankuni  8343  fin23lem29  8779  fin23lem30  8780  fin1a2lem12  8849  prdsds  15362  psss  16460  tgval2  19970  eltg4i  19974  unitgOLD  19982  ntrss2  20071  isopn3  20081  mretopd  20107  ordtbas  20207  cmpcov2  20404  tgcmp  20415  comppfsc  20546  alexsublem  21058  alexsubALTlem3  21063  alexsubALTlem4  21064  cldsubg  21124  bndth  21985  uniioombllem4  22543  uniioombllem5  22544  omssubadd  29137  omssubaddOLD  29141  cvmscld  30005  fnessref  31019  mblfinlem3  31944  mblfinlem4  31945  ismblfin  31946  mbfresfi  31952  cover2  32005
  Copyright terms: Public domain W3C validator