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 3938  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841

This theorem is referenced by:  unidif  4874  unixpss  5685  riotassuni  7156  unifpw  8829  fiuni  8894  rankuni  9294  fin23lem29  9765  fin23lem30  9766  fin1a2lem12  9835  prdsds  16739  psss  17826  tgval2  21566  eltg4i  21570  ntrss2  21667  isopn3  21676  mretopd  21702  ordtbas  21802  cmpcov2  22000  tgcmp  22011  comppfsc  22142  alexsublem  22654  alexsubALTlem3  22659  alexsubALTlem4  22660  cldsubg  22721  bndth  23564  uniioombllem4  24189  uniioombllem5  24190  omssubadd  31560  cvmscld  32522  fnessref  33707  inunissunidif  34658  mblfinlem3  34933  mblfinlem4  34934  ismblfin  34935  mbfresfi  34940  cover2  34991  salexct  42624  salgencntex  42633