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

Theorem eldifad 3361
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3359. (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 3359 . . 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 1756    \ cdif 3346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-dif 3352
This theorem is referenced by:  xpdifid  5287  unblem1  7585  cantnflem3  7920  cantnflem4  7921  cantnflem3OLD  7942  cantnflem4OLD  7943  oef1o  7951  oef1oOLD  7952  infxpenc  8205  infxpencOLD  8210  acndom2  8245  ackbij1lem18  8427  infpssrlem3  8495  fin23lem26  8515  fin23lem30  8532  pwfseqlem4a  8849  expclz  11911  symgextf  15943  pmtrfinv  15988  symggen  15997  efgsdmi  16250  efgs1b  16254  efgsp1  16255  efgsres  16256  efgredlemf  16259  efgredlemd  16262  efgredlem  16265  efgrelexlemb  16268  gsum2d2lem  16487  pgpfac1lem2  16598  pgpfac1lem3a  16599  pgpfac1lem3  16600  pgpfac1lem4  16601  isdrng2  16864  lvecinv  17216  lspsncmp  17219  lspsnne1  17220  lspsnnecom  17222  lspabs2  17223  lspsneu  17226  lspdisjb  17229  lspexch  17232  lspindp1  17236  lvecindp2  17242  lspsolv  17246  lspsnat  17248  lsppratlem1  17250  lsppratlem2  17251  fidomndrnglem  17400  frlmssuvc2  18242  frlmssuvc2OLD  18244  maducoeval2  18468  hauscmplem  19031  1stccnp  19088  imasdsf1olem  19970  rrxmetlem  20928  dvrec  21451  ftc1lem6  21535  elqaalem1  21807  elqaalem3  21809  ulmdvlem3  21889  abelthlem6  21923  abelthlem7a  21924  abelthlem7  21925  logtayl  22127  ftalem3  22434  lgsqrlem1  22702  lgsqrlem2  22703  lgsqrlem3  22704  lgsqrlem4  22705  lgseisenlem1  22710  lgseisenlem2  22711  lgseisenlem3  22712  lgseisenlem4  22713  lgseisen  22714  lgsquadlem2  22716  lgsquadlem3  22717  chebbnd1lem1  22740  dchrisum0re  22784  dchrisum0lema  22785  dchrisum0lem1b  22786  dchrisum0lem1  22787  dchrisum0lem2a  22788  dchrisum0lem2  22789  tgisline  23056  elntg  23252  uhgrass  23262  umgraex  23279  qqhval2  26433  esummono  26531  gsumesum  26532  measvuni  26650  sitgclg  26750  eulerpartlemsv2  26763  eulerpartlemsv3  26766  eulerpartlemgc  26767  eulerpartlemv  26769  signstfvneq0  26995  signstfvcl  26996  signstfveq0a  26999  signstfveq0  27000  signsvfn  27005  signsvtp  27006  signsvtn  27007  signlem0  27010  dmgmn0  27034  dmgmaddnn0  27035  dmgmdivn0  27036  lgamgulmlem2  27038  lgamgulmlem3  27039  lgamgulmlem5  27041  lgamgulmlem6  27042  lgamgulm2  27044  lgambdd  27045  lgamucov  27046  lgamcvg2  27063  gamcvg  27064  gamcvg2lem  27067  iprodgam  27528  rrndstprj2  28756  qirropth  29275  rmxyneg  29287  rmxm1  29301  rmxluc  29303  rmxdbl  29306  ltrmxnn0  29318  jm2.19lem1  29364  jm2.23  29371  rmxdiophlem  29390  aomclem2  29434  climrec  29802  climdivf  29811  stoweidlem34  29855  stoweidlem43  29864  lsatelbN  32747  lsatfixedN  32750  lkreqN  32911  lkrlspeqN  32912  dochnel2  35133  dochnel  35134  djhcvat42  35156  dochsnshp  35194  dochexmidat  35200  dochsnkr  35213  dochsnkr2  35214  dochsnkr2cl  35215  dochflcl  35216  dochfl1  35217  dochfln0  35218  lcfl6lem  35239  lcfl7lem  35240  lcfl8b  35245  lclkrlem2a  35248  lclkrlem2b  35249  lclkrlem2c  35250  lclkrlem2d  35251  lclkrlem2e  35252  lclkrlem2f  35253  lcfrlem14  35297  lcfrlem15  35298  lcfrlem16  35299  lcfrlem17  35300  lcfrlem18  35301  lcfrlem19  35302  lcfrlem20  35303  lcfrlem21  35304  lcfrlem23  35306  lcfrlem25  35308  lcfrlem26  35309  lcfrlem35  35318  lcfrlem36  35319  mapdn0  35410  mapdpglem29  35441  mapdpglem24  35445  baerlem3lem1  35448  baerlem5alem1  35449  baerlem5blem1  35450  baerlem3lem2  35451  baerlem5alem2  35452  baerlem5blem2  35453  baerlem5amN  35457  baerlem5bmN  35458  baerlem5abmN  35459  mapdindp0  35460  mapdindp1  35461  mapdindp2  35462  mapdindp3  35463  mapdindp4  35464  mapdheq2  35470  mapdheq4lem  35472  mapdheq4  35473  mapdh6lem1N  35474  mapdh6lem2N  35475  mapdh6aN  35476  mapdh6bN  35478  mapdh6cN  35479  mapdh6dN  35480  mapdh6eN  35481  mapdh6fN  35482  mapdh6gN  35483  mapdh6hN  35484  mapdh6iN  35485  mapdh7eN  35489  mapdh7cN  35490  mapdh7dN  35491  mapdh7fN  35492  mapdh75e  35493  mapdh75fN  35496  hvmaplfl  35508  mapdhvmap  35510  mapdh8aa  35517  mapdh8ab  35518  mapdh8ad  35520  mapdh8b  35521  mapdh8c  35522  mapdh8d0N  35523  mapdh8d  35524  mapdh8e  35525  mapdh9a  35531  hdmap1val2  35542  hdmap1eq  35543  hdmap1valc  35545  hdmap1eq2  35547  hdmap1eq4N  35548  hdmap1l6lem1  35549  hdmap1l6lem2  35550  hdmap1l6a  35551  hdmap1l6b  35553  hdmap1l6c  35554  hdmap1l6d  35555  hdmap1l6e  35556  hdmap1l6f  35557  hdmap1l6g  35558  hdmap1l6h  35559  hdmap1l6i  35560  hdmap1eulem  35565  hdmap1neglem1N  35569  hdmapcl  35574  hdmapval2lem  35575  hdmapval0  35577  hdmapeveclem  35578  hdmapevec  35579  hdmapval3lemN  35581  hdmapval3N  35582  hdmap10lem  35583  hdmap11lem1  35585  hdmap11lem2  35586  hdmapnzcl  35589  hdmaprnlem3N  35594  hdmaprnlem3uN  35595  hdmaprnlem4N  35597  hdmaprnlem7N  35599  hdmaprnlem8N  35600  hdmaprnlem9N  35601  hdmaprnlem3eN  35602  hdmaprnlem16N  35606  hdmap14lem1  35612  hdmap14lem2N  35613  hdmap14lem3  35614  hdmap14lem4a  35615  hdmap14lem6  35617  hdmap14lem8  35619  hdmap14lem9  35620  hdmap14lem10  35621  hdmap14lem11  35622  hdmap14lem12  35623  hgmaprnlem1N  35640  hgmaprnlem2N  35641  hgmaprnlem3N  35642  hgmaprnlem4N  35643  hdmapip1  35660  hdmapinvlem1  35662  hdmapinvlem2  35663  hdmapinvlem3  35664  hdmapinvlem4  35665  hdmapglem5  35666  hgmapvvlem1  35667  hgmapvvlem2  35668  hgmapvvlem3  35669  hdmapglem7a  35671  hdmapglem7b  35672  hdmapglem7  35673
  Copyright terms: Public domain W3C validator