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

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

Proof of Theorem difssd
StepHypRef Expression
1 difss 3947 . 2 (𝐴𝐵) ⊆ 𝐴
21a1i 11 1 (𝜑 → (𝐴𝐵) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3777  wss 3780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-dif 3783  df-in 3787  df-ss 3794
This theorem is referenced by:  uneqdifeq  4264  fofinf1o  8490  ackbij1lem12  9348  ssfin4  9427  enfin1ai  9501  fpwwe2  9760  wundif  9831  cshimadifsn  13819  fprodn0f  14962  rpnnen2lem11  15193  mrieqvlemd  16514  mrieqv2d  16524  symgextfo  18063  symgextres  18066  symgfixelsi  18076  pmtrdifellem1  18117  pmtrdifellem2  18118  dprdfeq0  18643  dpjf  18678  dpjlid  18682  dpjghm  18684  ablfac1eu  18694  islbs3  19384  lbsextlem4  19390  frlmsslss2  20345  frlmlbs  20367  mdetrlin  20640  mdetrsca  20641  mdetralt  20646  mdetmul  20661  smadiadetlem3lem0  20704  smadiadet  20709  clsval2  21089  hausllycmp  21532  qtoprest  21755  trfil3  21926  ufileu  21957  fclscf  22063  alexsublem  22082  blcld  22544  restmetu  22609  evth  22992  lebnumlem1  22994  lebnumlem2  22995  lebnumlem3  22996  cmmbl  23538  nulmbl2  23540  volinun  23550  volsup  23560  uniioombllem3  23589  uniioombllem5  23591  uniioombl  23593  itg1addlem5  23704  itg2cnlem2  23766  dvreslem  23910  dvres2lem  23911  dvaddbr  23938  dvmulbr  23939  dvrec  23955  dvexp3  23978  dveflem  23979  dvcnvrelem2  24018  uhgrspan1  26434  fprodeq02  29919  madjusmdetlem1  30241  indsum  30431  indsumin  30432  esumpad  30465  esumpad2  30466  measiun  30629  difelcarsg  30720  carsgclctunlem2  30729  tgoldbachgtde  31086  mthmpps  31824  dvreasin  33829  dvreacos  33830  areacirclem4  33834  ntrclsrcomplex  38851  clsk3nimkb  38856  ntrclsfveq1  38876  ntrclsiso  38883  ntrclsk2  38884  ntrclskb  38885  ntrclsk3  38886  ntrclsk13  38887  ntrneircomplex  38890  clsneircomplex  38919  clsneiel1  38924  neicvgrcomplex  38929  neicvgel1  38935  difmap  39904  difmapsn  39909  supminfxr2  40196  iccdifprioo  40241  limciccioolb  40351  lptioo2  40361  lptioo1  40362  limcicciooub  40367  dvdivcncf  40640  itgvol0  40681  itgcoscmulx  40682  itgsincmulx  40687  ismbl3  40700  stoweidlem28  40742  stoweidlem50  40764  dirkeritg  40816  dirkercncflem2  40818  dirkercncflem4  40820  fourierdlem39  40860  fourierdlem58  40878  fourierdlem68  40888  fourierdlem76  40896  fourierdlem102  40922  fourierdlem114  40934  pwsal  41032  salexct  41049  sge0fodjrnlem  41130  iundjiun  41174  meaunle  41178  meadjiunlem  41179  meaiunlelem  41182  meadif  41193  meaiuninclem  41194  meaiininclem  41200  carageniuncllem2  41236  caragencmpl  41249  hsphoidmvle2  41299  hsphoidmvle  41300  hoidmv1lelem2  41306  hspmbllem1  41340  hspmbllem3  41342  fdmdifeqresdif  42706  lincdifsn  42799  lincresunit2  42853  lincresunit3lem2  42855
  Copyright terms: Public domain W3C validator