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

Theorem unissd 4494
Description: Subclass relationship for subclass union. Deduction form of uniss 4490. (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 4490 . 2 (𝐴𝐵 𝐴 𝐵)
31, 2syl 17 1 (𝜑 𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3607   cuni 4468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-uni 4469
This theorem is referenced by:  dffv2  6310  onfununi  7483  fiuni  8375  dfac2a  8990  incexc  14613  incexc2  14614  isacs1i  16365  isacs3lem  17213  acsmapd  17225  acsmap2d  17226  dprdres  18473  dprd2da  18487  eltg3i  20813  unitg  20819  tgss  20820  tgcmp  21252  cmpfi  21259  alexsubALTlem4  21901  ptcmplem3  21905  ustbas2  22076  uniioombllem3  23399  shsupunss  28333  locfinref  30036  cmpcref  30045  dya2iocucvr  30474  omssubadd  30490  carsggect  30508  cvmscld  31381  fnemeet1  32486  fnejoin1  32488  onsucsuccmpi  32567  heibor1  33739  heiborlem10  33749  hbt  38017  caragenuni  41046  caragendifcl  41049  cnfsmf  41270  smfsssmf  41273  smfpimbor1lem2  41327  setrecsss  42772
  Copyright terms: Public domain W3C validator