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

Theorem unissi 4274
Description: Subclass relationship for subclass union. Inference form of uniss 4272. (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 4272 . 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 3481   U.cuni 4251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-in 3488  df-ss 3495  df-uni 4252
This theorem is referenced by:  unidif  4285  unixpss  5124  riotassuniOLD  6293  unifpw  7835  fiuni  7900  rankuni  8293  fin23lem29  8733  fin23lem30  8734  fin1a2lem12  8803  prdsds  14736  psss  15718  tgval2  19326  eltg4i  19330  unitg  19337  ntrss2  19426  isopn3  19435  mretopd  19461  ordtbas  19561  cmpcov2  19758  tgcmp  19769  comppfsc  19901  alexsublem  20412  alexsubALTlem3  20417  alexsubALTlem4  20418  cldsubg  20477  bndth  21326  uniioombllem4  21863  uniioombllem5  21864  cvmscld  28543  mblfinlem3  29980  mblfinlem4  29981  ismblfin  29982  mbfresfi  29988  fnessref  30102  cover2  30131
  Copyright terms: Public domain W3C validator