Theorem unissi 4849

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

Syntax hints:   ⊆ wss 3888  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-uni 4841

This theorem is referenced by:  unidif  4876  unixpss  5722  riotassuni  7282  unifpw  9131  fiuni  9196  rankuni  9630  fin23lem29  10106  fin23lem30  10107  fin1a2lem12  10176  prdsds  17184  psss  18307  tgval2  22115  eltg4i  22119  ntrss2  22217  isopn3  22226  mretopd  22252  ordtbas  22352  cmpcov2  22550  tgcmp  22561  comppfsc  22692  alexsublem  23204  alexsubALTlem3  23209  alexsubALTlem4  23210  cldsubg  23271  bndth  24130  uniioombllem4  24759  uniioombllem5  24760  omssubadd  32276  cvmscld  33244  fnessref  34555  inunissunidif  35555  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  mbfresfi  35832  cover2  35881  salexct  43880  salgencntex  43889