Theorem unissi 4461

Description: Subclass relationship for subclass union. Inference form of uniss 4458. (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

Step	Hyp	Ref	Expression
1		unissi.1	. 2 |- A C_ B
2		uniss 4458	. 2 |- ( A C_ B -> U. A C_ U. B )
3	1, 2	ax-mp 5	1 |- U. A C_ U. B

Syntax hints:   C_ wss 3574   U.cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-uni 4437

This theorem is referenced by:  unidif  4471  unixpss  5234  riotassuni  6648  unifpw  8269  fiuni  8334  rankuni  8726  fin23lem29  9163  fin23lem30  9164  fin1a2lem12  9233  prdsds  16124  psss  17214  tgval2  20760  eltg4i  20764  ntrss2  20861  isopn3  20870  mretopd  20896  ordtbas  20996  cmpcov2  21193  tgcmp  21204  comppfsc  21335  alexsublem  21848  alexsubALTlem3  21853  alexsubALTlem4  21854  cldsubg  21914  bndth  22757  uniioombllem4  23354  uniioombllem5  23355  omssubadd  30362  cvmscld  31255  fnessref  32352  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  mbfresfi  33456  cover2  33508  salexct  40552  salgencntex  40561