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

Theorem difssd 3771
Description: A difference of two classes is contained in the minuend. Deduction form of difss 3770. (Contributed by David Moews, 1-May-2017.)
Assertion
Ref Expression
difssd (𝜑 → (𝐴𝐵) ⊆ 𝐴)

Proof of Theorem difssd
StepHypRef Expression
1 difss 3770 . 2 (𝐴𝐵) ⊆ 𝐴
21a1i 11 1 (𝜑 → (𝐴𝐵) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3604  wss 3607
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-dif 3610  df-in 3614  df-ss 3621
This theorem is referenced by:  uneqdifeq  4090  fofinf1o  8282  ackbij1lem12  9091  ssfin4  9170  enfin1ai  9244  fpwwe2  9503  wundif  9574  cshimadifsn  13621  fprodn0f  14766  rpnnen2lem11  14997  mrieqvlemd  16336  mrieqv2d  16346  symgextfo  17888  symgextres  17891  symgfixelsi  17901  pmtrdifellem1  17942  pmtrdifellem2  17943  dprdfeq0  18467  dpjf  18502  dpjlid  18506  dpjghm  18508  ablfac1eu  18518  islbs3  19203  lbsextlem4  19209  frlmsslss2  20162  frlmlbs  20184  mdetrlin  20456  mdetrsca  20457  mdetralt  20462  mdetmul  20477  smadiadetlem3lem0  20519  smadiadet  20524  clsval2  20902  hausllycmp  21345  qtoprest  21568  trfil3  21739  ufileu  21770  fclscf  21876  alexsublem  21895  blcld  22357  restmetu  22422  evth  22805  lebnumlem1  22807  lebnumlem2  22808  lebnumlem3  22809  cmmbl  23348  nulmbl2  23350  volinun  23360  volsup  23370  uniioombllem3  23399  uniioombllem5  23401  uniioombl  23403  itg1addlem5  23512  itg2cnlem2  23574  dvreslem  23718  dvres2lem  23719  dvaddbr  23746  dvmulbr  23747  dvrec  23763  dvexp3  23786  dveflem  23787  dvcnvrelem2  23826  uhgrspan1  26240  fprodeq02  29697  madjusmdetlem1  30021  indsum  30211  indsumin  30212  esumpad  30245  esumpad2  30246  measiun  30409  difelcarsg  30500  carsgclctunlem2  30509  tgoldbachgtde  30866  mthmpps  31605  dvreasin  33628  dvreacos  33629  areacirclem4  33633  ntrclsrcomplex  38650  clsk3nimkb  38655  ntrclsfveq1  38675  ntrclsiso  38682  ntrclsk2  38683  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  ntrneircomplex  38689  clsneircomplex  38718  clsneiel1  38723  neicvgrcomplex  38728  neicvgel1  38734  difmap  39713  difmapsn  39718  supminfxr2  40012  iccdifprioo  40060  limciccioolb  40171  lptioo2  40181  lptioo1  40182  limcicciooub  40187  dvdivcncf  40460  itgvol0  40502  itgcoscmulx  40503  itgsincmulx  40508  ismbl3  40521  stoweidlem28  40563  stoweidlem50  40585  dirkeritg  40637  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem39  40681  fourierdlem58  40699  fourierdlem68  40709  fourierdlem76  40717  fourierdlem102  40743  fourierdlem114  40755  pwsal  40853  salexct  40870  sge0fodjrnlem  40951  iundjiun  40995  meaunle  40999  meadjiunlem  41000  meaiunlelem  41003  meadif  41014  meaiuninclem  41015  meaiininclem  41021  carageniuncllem2  41057  caragencmpl  41070  hsphoidmvle2  41120  hsphoidmvle  41121  hoidmv1lelem2  41127  hspmbllem1  41161  hspmbllem3  41163  fdmdifeqresdif  42445  lincdifsn  42538  lincresunit2  42592  lincresunit3lem2  42594
  Copyright terms: Public domain W3C validator