Theorem unissi 4876

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

Syntax hints:   ⊆ wss 3911  ∪ cuni 4867

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 3446  df-ss 3928  df-uni 4868

This theorem is referenced by:  unidif  4902  unixpss  5764  riotassuni  7366  unifpw  9282  fiuni  9355  rankuni  9792  fin23lem29  10270  fin23lem30  10271  fin1a2lem12  10340  prdsds  17403  psss  18515  tgval2  22819  eltg4i  22823  ntrss2  22920  isopn3  22929  mretopd  22955  ordtbas  23055  cmpcov2  23253  tgcmp  23264  comppfsc  23395  alexsublem  23907  alexsubALTlem3  23912  alexsubALTlem4  23913  cldsubg  23974  bndth  24833  uniioombllem4  25463  uniioombllem5  25464  omssubadd  34264  cvmscld  35233  fnessref  36318  inunissunidif  37336  mblfinlem3  37626  mblfinlem4  37627  ismblfin  37628  mbfresfi  37633  cover2  37682  salexct  46305  salgencntex  46314