Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  unissd Structured version   Visualization version   GIF version

Theorem unissd 4810
 Description: Subclass relationship for subclass union. Deduction form of uniss 4808. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
unissd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
unissd (𝜑 𝐴 𝐵)

Proof of Theorem unissd
StepHypRef Expression
1 unissd.1 . 2 (𝜑𝐴𝐵)
2 uniss 4808 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2syl 17 1 (𝜑 𝐴 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3881  ∪ cuni 4800 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801 This theorem is referenced by:  unieq  4811  dffv2  6733  onfununi  7961  fiuni  8876  dfac2a  9540  incexc  15184  incexc2  15185  isacs1i  16920  isacs3lem  17768  acsmapd  17780  acsmap2d  17781  dprdres  19143  dprd2da  19157  eltg3i  21566  unitg  21572  tgss  21573  tgcmp  22006  cmpfi  22013  alexsubALTlem4  22655  ptcmplem3  22659  ustbas2  22831  uniioombllem3  24189  shsupunss  29129  locfinref  31194  cmpcref  31203  dya2iocucvr  31652  omssubadd  31668  carsggect  31686  carsgclctun  31689  cvmscld  32630  fnemeet1  33824  fnejoin1  33826  onsucsuccmpi  33901  heibor1  35245  heiborlem10  35255  hbt  40069  pwsal  42952  prsal  42955  intsaluni  42964  caragenuni  43145  caragendifcl  43148  cnfsmf  43369  smfsssmf  43372  smfpimbor1lem2  43426  setrecsss  45225
 Copyright terms: Public domain W3C validator