MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldifad Unicode version

Theorem eldifad 3275
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3273. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
eldifad.1  |-  ( ph  ->  A  e.  ( B 
\  C ) )
Assertion
Ref Expression
eldifad  |-  ( ph  ->  A  e.  B )

Proof of Theorem eldifad
StepHypRef Expression
1 eldifad.1 . . 3  |-  ( ph  ->  A  e.  ( B 
\  C ) )
2 eldif 3273 . . 3  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
31, 2sylib 189 . 2  |-  ( ph  ->  ( A  e.  B  /\  -.  A  e.  C
) )
43simpld 446 1  |-  ( ph  ->  A  e.  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    e. wcel 1717    \ cdif 3260
This theorem is referenced by:  unblem1  7295  cantnflem3  7580  cantnflem4  7581  oef1o  7588  infxpenc  7832  acndom2  7868  ackbij1lem18  8050  infpssrlem3  8118  fin23lem26  8138  fin23lem30  8155  pwfseqlem4a  8469  expclz  11333  efgsdmi  15291  efgs1b  15295  efgsp1  15296  efgsres  15297  efgredlemf  15300  efgredlemd  15303  efgredlem  15306  efgrelexlemb  15309  gsum2d2lem  15474  pgpfac1lem2  15560  pgpfac1lem3a  15561  pgpfac1lem3  15562  pgpfac1lem4  15563  isdrng2  15772  lvecinv  16112  lspsncmp  16115  lspsnne1  16116  lspsnnecom  16118  lspabs2  16119  lspsneu  16122  lspdisjb  16125  lspexch  16128  lspindp1  16132  lvecindp2  16138  lspsolv  16142  lspsnat  16144  lsppratlem1  16146  lsppratlem2  16147  fidomndrnglem  16293  hauscmplem  17391  1stccnp  17446  imasdsf1olem  18311  dvrec  19708  ftc1lem6  19792  elqaalem1  20103  elqaalem3  20105  ulmdvlem3  20185  abelthlem6  20219  abelthlem7a  20220  abelthlem7  20221  logtayl  20418  ftalem3  20724  lgsqrlem1  20992  lgsqrlem2  20993  lgsqrlem3  20994  lgsqrlem4  20995  lgseisenlem1  21000  lgseisenlem2  21001  lgseisenlem3  21002  lgseisenlem4  21003  lgseisen  21004  lgsquadlem2  21006  lgsquadlem3  21007  chebbnd1lem1  21030  dchrisum0re  21074  dchrisum0lema  21075  dchrisum0lem1b  21076  dchrisum0lem1  21077  dchrisum0lem2a  21078  dchrisum0lem2  21079  uhgrass  21208  umgraex  21225  qqhval2  24165  esummono  24246  gsumesum  24247  measvuni  24362  dmgmn0  24589  dmgmaddnn0  24590  dmgmdivn0  24591  lgamgulmlem2  24593  lgamgulmlem3  24594  lgamgulmlem5  24596  lgamgulmlem6  24597  lgamgulm2  24599  lgambdd  24600  lgamucov  24601  lgamcvg2  24618  gamcvg  24619  gamcvg2lem  24622  rrndstprj2  26231  qirropth  26662  rmxyneg  26674  rmxm1  26688  rmxluc  26690  rmxdbl  26693  ltrmxnn0  26705  jm2.19lem1  26751  jm2.23  26758  rmxdiophlem  26777  aomclem2  26821  frlmssuvc2  26916  pmtrfinv  27071  symggen  27080  climrec  27397  climdivf  27406  stoweidlem34  27451  stoweidlem43  27460  lsatelbN  29121  lsatfixedN  29124  lkreqN  29285  lkrlspeqN  29286  dochnel2  31507  dochnel  31508  djhcvat42  31530  dochsnshp  31568  dochexmidat  31574  dochsnkr  31587  dochsnkr2  31588  dochsnkr2cl  31589  dochflcl  31590  dochfl1  31591  dochfln0  31592  lcfl6lem  31613  lcfl7lem  31614  lcfl8b  31619  lclkrlem2a  31622  lclkrlem2b  31623  lclkrlem2c  31624  lclkrlem2d  31625  lclkrlem2e  31626  lclkrlem2f  31627  lcfrlem14  31671  lcfrlem15  31672  lcfrlem16  31673  lcfrlem17  31674  lcfrlem18  31675  lcfrlem19  31676  lcfrlem20  31677  lcfrlem21  31678  lcfrlem23  31680  lcfrlem25  31682  lcfrlem26  31683  lcfrlem35  31692  lcfrlem36  31693  mapdn0  31784  mapdpglem29  31815  mapdpglem24  31819  baerlem3lem1  31822  baerlem5alem1  31823  baerlem5blem1  31824  baerlem3lem2  31825  baerlem5alem2  31826  baerlem5blem2  31827  baerlem5amN  31831  baerlem5bmN  31832  baerlem5abmN  31833  mapdindp0  31834  mapdindp1  31835  mapdindp2  31836  mapdindp3  31837  mapdindp4  31838  mapdheq2  31844  mapdheq4lem  31846  mapdheq4  31847  mapdh6lem1N  31848  mapdh6lem2N  31849  mapdh6aN  31850  mapdh6bN  31852  mapdh6cN  31853  mapdh6dN  31854  mapdh6eN  31855  mapdh6fN  31856  mapdh6gN  31857  mapdh6hN  31858  mapdh6iN  31859  mapdh7eN  31863  mapdh7cN  31864  mapdh7dN  31865  mapdh7fN  31866  mapdh75e  31867  mapdh75fN  31870  hvmaplfl  31882  mapdhvmap  31884  mapdh8aa  31891  mapdh8ab  31892  mapdh8ad  31894  mapdh8b  31895  mapdh8c  31896  mapdh8d0N  31897  mapdh8d  31898  mapdh8e  31899  mapdh9a  31905  hdmap1val2  31916  hdmap1eq  31917  hdmap1valc  31919  hdmap1eq2  31921  hdmap1eq4N  31922  hdmap1l6lem1  31923  hdmap1l6lem2  31924  hdmap1l6a  31925  hdmap1l6b  31927  hdmap1l6c  31928  hdmap1l6d  31929  hdmap1l6e  31930  hdmap1l6f  31931  hdmap1l6g  31932  hdmap1l6h  31933  hdmap1l6i  31934  hdmap1eulem  31939  hdmap1neglem1N  31943  hdmapcl  31948  hdmapval2lem  31949  hdmapval0  31951  hdmapeveclem  31952  hdmapevec  31953  hdmapval3lemN  31955  hdmapval3N  31956  hdmap10lem  31957  hdmap11lem1  31959  hdmap11lem2  31960  hdmapnzcl  31963  hdmaprnlem3N  31968  hdmaprnlem3uN  31969  hdmaprnlem4N  31971  hdmaprnlem7N  31973  hdmaprnlem8N  31974  hdmaprnlem9N  31975  hdmaprnlem3eN  31976  hdmaprnlem16N  31980  hdmap14lem1  31986  hdmap14lem2N  31987  hdmap14lem3  31988  hdmap14lem4a  31989  hdmap14lem6  31991  hdmap14lem8  31993  hdmap14lem9  31994  hdmap14lem10  31995  hdmap14lem11  31996  hdmap14lem12  31997  hgmaprnlem1N  32014  hgmaprnlem2N  32015  hgmaprnlem3N  32016  hgmaprnlem4N  32017  hdmapip1  32034  hdmapinvlem1  32036  hdmapinvlem2  32037  hdmapinvlem3  32038  hdmapinvlem4  32039  hdmapglem5  32040  hgmapvvlem1  32041  hgmapvvlem2  32042  hgmapvvlem3  32043  hdmapglem7a  32045  hdmapglem7b  32046  hdmapglem7  32047
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-dif 3266
  Copyright terms: Public domain W3C validator