Theorem unissi 4231

Description: Subclass relationship for subclass union. Inference form of uniss 4229. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
unissi.1

Assertion

Ref	Expression
unissi

Proof of Theorem unissi

Step	Hyp	Ref	Expression
1		unissi.1	. 2
2		uniss 4229	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  C_wss 3442  U.cuni 4208

This theorem is referenced by:  unidif  4242  unixpss  5072  riotassuniOLD  6220  unifpw  7749  fiuni  7814  rankuni  8207  fin23lem29  8647  fin23lem30  8648  fin1a2lem12  8717  prdsds  14561  psss  15543  tgval2  18960  eltg4i  18964  unitg  18971  ntrss2  19060  isopn3  19069  mretopd  19095  ordtbas  19195  cmpcov2  19392  tgcmp  19403  alexsublem  20015  alexsubALTlem3  20020  alexsubALTlem4  20021  cldsubg  20080  bndth  20929  uniioombllem4  21466  uniioombllem5  21467  cvmscld  27618  mblfinlem3  28890  mblfinlem4  28891  ismblfin  28892  mbfresfi  28898  fnessref  29025  comppfsc  29039  cover2  29067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083  df-in 3449  df-ss 3456  df-uni 4209