Theorem unissi 4940

Description: Subclass relationship for subclass union. Inference form of uniss 4939. (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 4939	. 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 ⊆ ∪ 𝐵

Syntax hints:   ⊆ wss 3976  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932

This theorem is referenced by:  unidif  4966  unixpss  5834  riotassuni  7445  unifpw  9425  fiuni  9497  rankuni  9932  fin23lem29  10410  fin23lem30  10411  fin1a2lem12  10480  prdsds  17524  psss  18650  tgval2  22984  eltg4i  22988  ntrss2  23086  isopn3  23095  mretopd  23121  ordtbas  23221  cmpcov2  23419  tgcmp  23430  comppfsc  23561  alexsublem  24073  alexsubALTlem3  24078  alexsubALTlem4  24079  cldsubg  24140  bndth  25009  uniioombllem4  25640  uniioombllem5  25641  omssubadd  34265  cvmscld  35241  fnessref  36323  inunissunidif  37341  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  mbfresfi  37626  cover2  37675  salexct  46255  salgencntex  46264