Theorem unissi 4867

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

Syntax hints:   ⊆ wss 3903  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-uni 4859

This theorem is referenced by:  unidif  4892  unixpss  5753  riotassuni  7346  unifpw  9245  fiuni  9318  rankuni  9759  fin23lem29  10235  fin23lem30  10236  fin1a2lem12  10305  prdsds  17368  psss  18486  tgval2  22841  eltg4i  22845  ntrss2  22942  isopn3  22951  mretopd  22977  ordtbas  23077  cmpcov2  23275  tgcmp  23286  comppfsc  23417  alexsublem  23929  alexsubALTlem3  23934  alexsubALTlem4  23935  cldsubg  23996  bndth  24855  uniioombllem4  25485  uniioombllem5  25486  omssubadd  34268  cvmscld  35246  fnessref  36331  inunissunidif  37349  mblfinlem3  37639  mblfinlem4  37640  ismblfin  37641  mbfresfi  37646  cover2  37695  salexct  46315  salgencntex  46324