Theorem unissi 4613

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

Syntax hints:   ⊆ wss 3715  ∪ cuni 4588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729  df-uni 4589

This theorem is referenced by:  unidif  4623  unixpss  5390  riotassuni  6811  unifpw  8434  fiuni  8499  rankuni  8899  fin23lem29  9355  fin23lem30  9356  fin1a2lem12  9425  prdsds  16326  psss  17415  tgval2  20962  eltg4i  20966  ntrss2  21063  isopn3  21072  mretopd  21098  ordtbas  21198  cmpcov2  21395  tgcmp  21406  comppfsc  21537  alexsublem  22049  alexsubALTlem3  22054  alexsubALTlem4  22055  cldsubg  22115  bndth  22958  uniioombllem4  23554  uniioombllem5  23555  omssubadd  30671  cvmscld  31562  fnessref  32658  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  mbfresfi  33769  cover2  33821  salexct  41055  salgencntex  41064