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

Theorem eldifad 3328
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3326. (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 3326 . . 3  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
31, 2sylib 196 . 2  |-  ( ph  ->  ( A  e.  B  /\  -.  A  e.  C
) )
43simpld 456 1  |-  ( ph  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    e. wcel 1755    \ cdif 3313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319
This theorem is referenced by:  xpdifid  5254  unblem1  7552  cantnflem3  7887  cantnflem4  7888  cantnflem3OLD  7909  cantnflem4OLD  7910  oef1o  7918  oef1oOLD  7919  infxpenc  8172  infxpencOLD  8177  acndom2  8212  ackbij1lem18  8394  infpssrlem3  8462  fin23lem26  8482  fin23lem30  8499  pwfseqlem4a  8815  expclz  11873  symgextf  15901  pmtrfinv  15946  symggen  15955  efgsdmi  16208  efgs1b  16212  efgsp1  16213  efgsres  16214  efgredlemf  16217  efgredlemd  16220  efgredlem  16223  efgrelexlemb  16226  gsum2d2lem  16438  pgpfac1lem2  16549  pgpfac1lem3a  16550  pgpfac1lem3  16551  pgpfac1lem4  16552  isdrng2  16765  lvecinv  17115  lspsncmp  17118  lspsnne1  17119  lspsnnecom  17121  lspabs2  17122  lspsneu  17125  lspdisjb  17128  lspexch  17131  lspindp1  17135  lvecindp2  17141  lspsolv  17145  lspsnat  17147  lsppratlem1  17149  lsppratlem2  17150  fidomndrnglem  17299  frlmssuvc2  18061  frlmssuvc2OLD  18063  maducoeval2  18287  hauscmplem  18850  1stccnp  18907  imasdsf1olem  19789  rrxmetlem  20747  dvrec  21270  ftc1lem6  21354  elqaalem1  21669  elqaalem3  21671  ulmdvlem3  21751  abelthlem6  21785  abelthlem7a  21786  abelthlem7  21787  logtayl  21989  ftalem3  22296  lgsqrlem1  22564  lgsqrlem2  22565  lgsqrlem3  22566  lgsqrlem4  22567  lgseisenlem1  22572  lgseisenlem2  22573  lgseisenlem3  22574  lgseisenlem4  22575  lgseisen  22576  lgsquadlem2  22578  lgsquadlem3  22579  chebbnd1lem1  22602  dchrisum0re  22646  dchrisum0lema  22647  dchrisum0lem1b  22648  dchrisum0lem1  22649  dchrisum0lem2a  22650  dchrisum0lem2  22651  tgisline  22905  elntg  23052  uhgrass  23062  umgraex  23079  qqhval2  26264  esummono  26362  gsumesum  26363  measvuni  26481  sitgclg  26575  eulerpartlemsv2  26588  eulerpartlemsv3  26591  eulerpartlemgc  26592  eulerpartlemv  26594  signstfvneq0  26820  signstfvcl  26821  signstfveq0a  26824  signstfveq0  26825  signsvfn  26830  signsvtp  26831  signsvtn  26832  signlem0  26835  dmgmn0  26859  dmgmaddnn0  26860  dmgmdivn0  26861  lgamgulmlem2  26863  lgamgulmlem3  26864  lgamgulmlem5  26866  lgamgulmlem6  26867  lgamgulm2  26869  lgambdd  26870  lgamucov  26871  lgamcvg2  26888  gamcvg  26889  gamcvg2lem  26892  iprodgam  27352  rrndstprj2  28571  qirropth  29091  rmxyneg  29103  rmxm1  29117  rmxluc  29119  rmxdbl  29122  ltrmxnn0  29134  jm2.19lem1  29180  jm2.23  29187  rmxdiophlem  29206  aomclem2  29250  climrec  29619  climdivf  29628  stoweidlem34  29672  stoweidlem43  29681  lsatelbN  32221  lsatfixedN  32224  lkreqN  32385  lkrlspeqN  32386  dochnel2  34607  dochnel  34608  djhcvat42  34630  dochsnshp  34668  dochexmidat  34674  dochsnkr  34687  dochsnkr2  34688  dochsnkr2cl  34689  dochflcl  34690  dochfl1  34691  dochfln0  34692  lcfl6lem  34713  lcfl7lem  34714  lcfl8b  34719  lclkrlem2a  34722  lclkrlem2b  34723  lclkrlem2c  34724  lclkrlem2d  34725  lclkrlem2e  34726  lclkrlem2f  34727  lcfrlem14  34771  lcfrlem15  34772  lcfrlem16  34773  lcfrlem17  34774  lcfrlem18  34775  lcfrlem19  34776  lcfrlem20  34777  lcfrlem21  34778  lcfrlem23  34780  lcfrlem25  34782  lcfrlem26  34783  lcfrlem35  34792  lcfrlem36  34793  mapdn0  34884  mapdpglem29  34915  mapdpglem24  34919  baerlem3lem1  34922  baerlem5alem1  34923  baerlem5blem1  34924  baerlem3lem2  34925  baerlem5alem2  34926  baerlem5blem2  34927  baerlem5amN  34931  baerlem5bmN  34932  baerlem5abmN  34933  mapdindp0  34934  mapdindp1  34935  mapdindp2  34936  mapdindp3  34937  mapdindp4  34938  mapdheq2  34944  mapdheq4lem  34946  mapdheq4  34947  mapdh6lem1N  34948  mapdh6lem2N  34949  mapdh6aN  34950  mapdh6bN  34952  mapdh6cN  34953  mapdh6dN  34954  mapdh6eN  34955  mapdh6fN  34956  mapdh6gN  34957  mapdh6hN  34958  mapdh6iN  34959  mapdh7eN  34963  mapdh7cN  34964  mapdh7dN  34965  mapdh7fN  34966  mapdh75e  34967  mapdh75fN  34970  hvmaplfl  34982  mapdhvmap  34984  mapdh8aa  34991  mapdh8ab  34992  mapdh8ad  34994  mapdh8b  34995  mapdh8c  34996  mapdh8d0N  34997  mapdh8d  34998  mapdh8e  34999  mapdh9a  35005  hdmap1val2  35016  hdmap1eq  35017  hdmap1valc  35019  hdmap1eq2  35021  hdmap1eq4N  35022  hdmap1l6lem1  35023  hdmap1l6lem2  35024  hdmap1l6a  35025  hdmap1l6b  35027  hdmap1l6c  35028  hdmap1l6d  35029  hdmap1l6e  35030  hdmap1l6f  35031  hdmap1l6g  35032  hdmap1l6h  35033  hdmap1l6i  35034  hdmap1eulem  35039  hdmap1neglem1N  35043  hdmapcl  35048  hdmapval2lem  35049  hdmapval0  35051  hdmapeveclem  35052  hdmapevec  35053  hdmapval3lemN  35055  hdmapval3N  35056  hdmap10lem  35057  hdmap11lem1  35059  hdmap11lem2  35060  hdmapnzcl  35063  hdmaprnlem3N  35068  hdmaprnlem3uN  35069  hdmaprnlem4N  35071  hdmaprnlem7N  35073  hdmaprnlem8N  35074  hdmaprnlem9N  35075  hdmaprnlem3eN  35076  hdmaprnlem16N  35080  hdmap14lem1  35086  hdmap14lem2N  35087  hdmap14lem3  35088  hdmap14lem4a  35089  hdmap14lem6  35091  hdmap14lem8  35093  hdmap14lem9  35094  hdmap14lem10  35095  hdmap14lem11  35096  hdmap14lem12  35097  hgmaprnlem1N  35114  hgmaprnlem2N  35115  hgmaprnlem3N  35116  hgmaprnlem4N  35117  hdmapip1  35134  hdmapinvlem1  35136  hdmapinvlem2  35137  hdmapinvlem3  35138  hdmapinvlem4  35139  hdmapglem5  35140  hgmapvvlem1  35141  hgmapvvlem2  35142  hgmapvvlem3  35143  hdmapglem7a  35145  hdmapglem7b  35146  hdmapglem7  35147
  Copyright terms: Public domain W3C validator