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 3471   U.cuni 4251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478  df-ss 3485  df-uni 4252
This theorem is referenced by:  unidif  4285  unixpss  5127  riotassuniOLD  6294  unifpw  7841  fiuni  7906  rankuni  8298  fin23lem29  8738  fin23lem30  8739  fin1a2lem12  8808  prdsds  14880  psss  15970  tgval2  19583  eltg4i  19587  unitgOLD  19595  ntrss2  19684  isopn3  19693  mretopd  19719  ordtbas  19819  cmpcov2  20016  tgcmp  20027  comppfsc  20158  alexsublem  20669  alexsubALTlem3  20674  alexsubALTlem4  20675  cldsubg  20734  bndth  21583  uniioombllem4  22120  uniioombllem5  22121  omssubadd  28432  cvmscld  28893  mblfinlem3  30215  mblfinlem4  30216  ismblfin  30217  mbfresfi  30223  fnessref  30337  cover2  30366
  Copyright terms: Public domain W3C validator