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

Theorem eldifad 3488
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3486. (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 3486 . . 3  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
31, 2sylib 196 . 2  |-  ( ph  ->  ( A  e.  B  /\  -.  A  e.  C
) )
43simpld 459 1  |-  ( ph  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    e. wcel 1767    \ cdif 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479
This theorem is referenced by:  xpdifid  5435  unblem1  7772  cantnflem3  8110  cantnflem4  8111  cantnflem3OLD  8132  cantnflem4OLD  8133  oef1o  8141  oef1oOLD  8142  infxpenc  8395  infxpencOLD  8400  acndom2  8435  ackbij1lem18  8617  infpssrlem3  8685  fin23lem26  8705  fin23lem30  8722  pwfseqlem4a  9039  expclz  12159  symgextf  16247  pmtrfinv  16292  symggen  16301  efgsdmi  16556  efgs1b  16560  efgsp1  16561  efgsres  16562  efgredlemf  16565  efgredlemd  16568  efgredlem  16571  efgrelexlemb  16574  gsum2d2lem  16804  pgpfac1lem2  16928  pgpfac1lem3a  16929  pgpfac1lem3  16930  pgpfac1lem4  16931  isdrng2  17206  lvecinv  17559  lspsncmp  17562  lspsnne1  17563  lspsnnecom  17565  lspabs2  17566  lspsneu  17569  lspdisjb  17572  lspexch  17575  lspindp1  17579  lvecindp2  17585  lspsolv  17589  lspsnat  17591  lsppratlem1  17593  lsppratlem2  17594  fidomndrnglem  17754  frlmssuvc2  18621  frlmssuvc2OLD  18623  maducoeval2  18937  hauscmplem  19700  1stccnp  19757  imasdsf1olem  20639  rrxmetlem  21597  dvrec  22121  ftc1lem6  22205  elqaalem1  22477  elqaalem3  22479  ulmdvlem3  22559  abelthlem6  22593  abelthlem7a  22594  abelthlem7  22595  logtayl  22797  ftalem3  23104  lgsqrlem1  23372  lgsqrlem2  23373  lgsqrlem3  23374  lgsqrlem4  23375  lgseisenlem1  23380  lgseisenlem2  23381  lgseisenlem3  23382  lgseisenlem4  23383  lgseisen  23384  lgsquadlem2  23386  lgsquadlem3  23387  chebbnd1lem1  23410  dchrisum0re  23454  dchrisum0lema  23455  dchrisum0lem1b  23456  dchrisum0lem1  23457  dchrisum0lem2a  23458  dchrisum0lem2  23459  tgisline  23749  elntg  23991  uhgrass  24010  umgraex  24027  qqhval2  27627  qtophaus  27665  esummono  27734  gsumesum  27735  measvuni  27853  sitgclg  27952  eulerpartlemsv2  27965  eulerpartlemsv3  27968  eulerpartlemgc  27969  eulerpartlemv  27971  signstfvneq0  28197  signstfvcl  28198  signstfveq0a  28201  signstfveq0  28202  signsvfn  28207  signsvtp  28208  signsvtn  28209  signlem0  28212  dmgmn0  28236  dmgmaddnn0  28237  dmgmdivn0  28238  lgamgulmlem2  28240  lgamgulmlem3  28241  lgamgulmlem5  28243  lgamgulmlem6  28244  lgamgulm2  28246  lgambdd  28247  lgamucov  28248  lgamcvg2  28265  gamcvg  28266  gamcvg2lem  28269  iprodgam  28730  rrndstprj2  29958  qirropth  30476  rmxyneg  30488  rmxm1  30502  rmxluc  30504  rmxdbl  30507  ltrmxnn0  30519  jm2.19lem1  30563  jm2.23  30570  rmxdiophlem  30589  aomclem2  30633  dstregt0  31068  climrec  31173  climdivf  31182  islpcn  31209  0ellimcdiv  31219  reclimc  31223  divlimc  31226  divcncf  31250  dvmptdiv  31275  fperdvper  31276  dvdivf  31280  stoweidlem34  31362  stoweidlem43  31371  fourierdlem62  31497  uhgss  31864  lsatelbN  33821  lsatfixedN  33824  lkreqN  33985  lkrlspeqN  33986  dochnel2  36207  dochnel  36208  djhcvat42  36230  dochsnshp  36268  dochexmidat  36274  dochsnkr  36287  dochsnkr2  36288  dochsnkr2cl  36289  dochflcl  36290  dochfl1  36291  dochfln0  36292  lcfl6lem  36313  lcfl7lem  36314  lcfl8b  36319  lclkrlem2a  36322  lclkrlem2b  36323  lclkrlem2c  36324  lclkrlem2d  36325  lclkrlem2e  36326  lclkrlem2f  36327  lcfrlem14  36371  lcfrlem15  36372  lcfrlem16  36373  lcfrlem17  36374  lcfrlem18  36375  lcfrlem19  36376  lcfrlem20  36377  lcfrlem21  36378  lcfrlem23  36380  lcfrlem25  36382  lcfrlem26  36383  lcfrlem35  36392  lcfrlem36  36393  mapdn0  36484  mapdpglem29  36515  mapdpglem24  36519  baerlem3lem1  36522  baerlem5alem1  36523  baerlem5blem1  36524  baerlem3lem2  36525  baerlem5alem2  36526  baerlem5blem2  36527  baerlem5amN  36531  baerlem5bmN  36532  baerlem5abmN  36533  mapdindp0  36534  mapdindp1  36535  mapdindp2  36536  mapdindp3  36537  mapdindp4  36538  mapdheq2  36544  mapdheq4lem  36546  mapdheq4  36547  mapdh6lem1N  36548  mapdh6lem2N  36549  mapdh6aN  36550  mapdh6bN  36552  mapdh6cN  36553  mapdh6dN  36554  mapdh6eN  36555  mapdh6fN  36556  mapdh6gN  36557  mapdh6hN  36558  mapdh6iN  36559  mapdh7eN  36563  mapdh7cN  36564  mapdh7dN  36565  mapdh7fN  36566  mapdh75e  36567  mapdh75fN  36570  hvmaplfl  36582  mapdhvmap  36584  mapdh8aa  36591  mapdh8ab  36592  mapdh8ad  36594  mapdh8b  36595  mapdh8c  36596  mapdh8d0N  36597  mapdh8d  36598  mapdh8e  36599  mapdh9a  36605  hdmap1val2  36616  hdmap1eq  36617  hdmap1valc  36619  hdmap1eq2  36621  hdmap1eq4N  36622  hdmap1l6lem1  36623  hdmap1l6lem2  36624  hdmap1l6a  36625  hdmap1l6b  36627  hdmap1l6c  36628  hdmap1l6d  36629  hdmap1l6e  36630  hdmap1l6f  36631  hdmap1l6g  36632  hdmap1l6h  36633  hdmap1l6i  36634  hdmap1eulem  36639  hdmap1neglem1N  36643  hdmapcl  36648  hdmapval2lem  36649  hdmapval0  36651  hdmapeveclem  36652  hdmapevec  36653  hdmapval3lemN  36655  hdmapval3N  36656  hdmap10lem  36657  hdmap11lem1  36659  hdmap11lem2  36660  hdmapnzcl  36663  hdmaprnlem3N  36668  hdmaprnlem3uN  36669  hdmaprnlem4N  36671  hdmaprnlem7N  36673  hdmaprnlem8N  36674  hdmaprnlem9N  36675  hdmaprnlem3eN  36676  hdmaprnlem16N  36680  hdmap14lem1  36686  hdmap14lem2N  36687  hdmap14lem3  36688  hdmap14lem4a  36689  hdmap14lem6  36691  hdmap14lem8  36693  hdmap14lem9  36694  hdmap14lem10  36695  hdmap14lem11  36696  hdmap14lem12  36697  hgmaprnlem1N  36714  hgmaprnlem2N  36715  hgmaprnlem3N  36716  hgmaprnlem4N  36717  hdmapip1  36734  hdmapinvlem1  36736  hdmapinvlem2  36737  hdmapinvlem3  36738  hdmapinvlem4  36739  hdmapglem5  36740  hgmapvvlem1  36741  hgmapvvlem2  36742  hgmapvvlem3  36743  hdmapglem7a  36745  hdmapglem7b  36746  hdmapglem7  36747
  Copyright terms: Public domain W3C validator