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

Theorem unissd 4917
Description: Subclass relationship for subclass union. Deduction form of uniss 4915. (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 4915 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2syl 17 1 (𝜑 𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3951   cuni 4907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908
This theorem is referenced by:  unieq  4918  dffv2  7004  onfununi  8381  fiuni  9468  dfac2a  10170  incexc  15873  incexc2  15874  isacs1i  17700  isacs3lem  18587  acsmapd  18599  acsmap2d  18600  dprdres  20048  dprd2da  20062  eltg3i  22968  unitg  22974  tgss  22975  tgcmp  23409  cmpfi  23416  alexsubALTlem4  24058  ptcmplem3  24062  ustbas2  24234  uniioombllem3  25620  madess  27915  shsupunss  31365  locfinref  33840  cmpcref  33849  dya2iocucvr  34286  omssubadd  34302  carsggect  34320  carsgclctun  34323  cvmscld  35278  fnemeet1  36367  fnejoin1  36369  onsucsuccmpi  36444  heibor1  37817  heiborlem10  37827  hbt  43142  pwsal  46330  prsal  46333  intsaluni  46344  caragenuni  46526  caragendifcl  46529  cnfsmf  46755  smfsssmf  46758  smfpimbor1lem2  46814  toplatglb  48890  setrecsss  49220
  Copyright terms: Public domain W3C validator