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

Theorem unissi 4062
Description: Subclass relationship for subclass union. Inference form of uniss 4060. (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 4060 . 2  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
31, 2ax-mp 5 1  |-  U. A  C_ 
U. B
Colors of variables: wff set class
Syntax hints:    C_ wss 3306   U.cuni 4039
This theorem is referenced by:  unidif  4071  unixpss  5017  riotassuni  6617  unifpw  7438  fiuni  7462  rankuni  7818  fin23lem29  8252  fin23lem30  8253  fin1a2lem12  8322  prdsds  13717  psss  14677  tgval2  17052  eltg4i  17056  unitg  17063  ntrss2  17152  isopn3  17161  mretopd  17187  ordtbas  17287  cmpcov2  17484  tgcmp  17495  alexsublem  18106  alexsubALTlem3  18111  alexsubALTlem4  18112  cldsubg  18171  bndth  19014  uniioombllem4  19509  uniioombllem5  19510  cvmscld  24991  mblfinlem3  26281  mblfinlem4  26282  ismblfin  26283  mbfresfi  26289  fnessref  26411  comppfsc  26425  cover2  26453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-in 3313  df-ss 3320  df-uni 4040
  Copyright terms: Public domain W3C validator