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

Theorem unissd 4398
Description: Subclass relationship for subclass union. Deduction form of uniss 4394. (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 4394 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2syl 17 1 (𝜑 𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  dffv2  6181  onfununi  7325  fiuni  8217  dfac2a  8835  incexc  14408  incexc2  14409  isacs1i  16141  isacs3lem  16989  acsmapd  17001  acsmap2d  17002  dprdres  18250  dprd2da  18264  eltg3i  20576  unitg  20582  tgss  20583  tgcmp  21014  cmpfi  21021  alexsubALTlem4  21664  ptcmplem3  21668  ustbas2  21839  uniioombllem3  23159  shsupunss  27589  locfinref  29236  cmpcref  29245  dya2iocucvr  29673  omssubadd  29689  carsggect  29707  cvmscld  30509  nofulllem3  31103  fnemeet1  31531  fnejoin1  31533  onsucsuccmpi  31612  heibor1  32779  heiborlem10  32789  hbt  36719  caragenuni  39401  caragendifcl  39404  cnfsmf  39627  smfsssmf  39630  smfpimbor1lem2  39684
  Copyright terms: Public domain W3C validator