Theorem unissi 4397

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

Syntax hints:   ⊆ wss 3540  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-uni 4373

This theorem is referenced by:  unidif  4407  unixpss  5157  riotassuni  6547  unifpw  8152  fiuni  8217  rankuni  8609  fin23lem29  9046  fin23lem30  9047  fin1a2lem12  9116  prdsds  15947  psss  17037  tgval2  20571  eltg4i  20575  ntrss2  20671  isopn3  20680  mretopd  20706  ordtbas  20806  cmpcov2  21003  tgcmp  21014  comppfsc  21145  alexsublem  21658  alexsubALTlem3  21663  alexsubALTlem4  21664  cldsubg  21724  bndth  22565  uniioombllem4  23160  uniioombllem5  23161  omssubadd  29689  cvmscld  30509  fnessref  31522  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  mbfresfi  32626  cover2  32678  salexct  39228  salgencntex  39237