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

Theorem unissd 4433
Description: Subclass relationship for subclass union. Deduction form of uniss 4429. (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 4429 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2syl 17 1 (𝜑 𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3560   cuni 4407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-in 3567  df-ss 3574  df-uni 4408
This theorem is referenced by:  dffv2  6229  onfununi  7384  fiuni  8279  dfac2a  8897  incexc  14489  incexc2  14490  isacs1i  16234  isacs3lem  17082  acsmapd  17094  acsmap2d  17095  dprdres  18343  dprd2da  18357  eltg3i  20671  unitg  20677  tgss  20678  tgcmp  21109  cmpfi  21116  alexsubALTlem4  21759  ptcmplem3  21763  ustbas2  21934  uniioombllem3  23254  shsupunss  28045  locfinref  29682  cmpcref  29691  dya2iocucvr  30119  omssubadd  30135  carsggect  30153  cvmscld  30955  fnemeet1  31995  fnejoin1  31997  onsucsuccmpi  32076  heibor1  33227  heiborlem10  33237  hbt  37167  caragenuni  40019  caragendifcl  40022  cnfsmf  40243  smfsssmf  40246  smfpimbor1lem2  40300
  Copyright terms: Public domain W3C validator