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

Theorem eldifad 3401
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3399. (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 3399 . . 3  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
31, 2sylib 196 . 2  |-  ( ph  ->  ( A  e.  B  /\  -.  A  e.  C
) )
43simpld 457 1  |-  ( ph  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367    e. wcel 1826    \ cdif 3386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-dif 3392
This theorem is referenced by:  xpdifid  5345  unblem1  7687  cantnflem3  8023  cantnflem4  8024  cantnflem3OLD  8045  cantnflem4OLD  8046  oef1o  8054  oef1oOLD  8055  infxpenc  8308  infxpencOLD  8313  acndom2  8348  ackbij1lem18  8530  infpssrlem3  8598  fin23lem26  8618  fin23lem30  8635  pwfseqlem4a  8950  expclz  12094  symgextf  16559  pmtrfinv  16603  symggen  16612  efgsdmi  16867  efgs1b  16871  efgsp1  16872  efgsres  16873  efgredlemf  16876  efgredlemd  16879  efgredlem  16882  efgrelexlemb  16885  gsum2d2lem  17115  pgpfac1lem2  17239  pgpfac1lem3a  17240  pgpfac1lem3  17241  pgpfac1lem4  17242  isdrng2  17519  lvecinv  17872  lspsncmp  17875  lspsnne1  17876  lspsnnecom  17878  lspabs2  17879  lspsneu  17882  lspdisjb  17885  lspexch  17888  lspindp1  17892  lvecindp2  17898  lspsolv  17902  lspsnat  17904  lsppratlem1  17906  lsppratlem2  17907  fidomndrnglem  18068  frlmssuvc2  18915  maducoeval2  19227  hauscmplem  19992  1stccnp  20048  imasdsf1olem  20961  rrxmetlem  21919  dvrec  22443  ftc1lem6  22527  elqaalem1  22800  elqaalem3  22802  ulmdvlem3  22882  abelthlem6  22916  abelthlem7a  22917  abelthlem7  22918  logtayl  23128  ftalem3  23465  lgsqrlem1  23733  lgsqrlem2  23734  lgsqrlem3  23735  lgsqrlem4  23736  lgseisenlem1  23741  lgseisenlem2  23742  lgseisenlem3  23743  lgseisenlem4  23744  lgseisen  23745  lgsquadlem2  23747  lgsquadlem3  23748  chebbnd1lem1  23771  dchrisum0re  23815  dchrisum0lema  23816  dchrisum0lem1b  23817  dchrisum0lem1  23818  dchrisum0lem2a  23819  dchrisum0lem2  23820  tgisline  24127  elntg  24408  uhgrass  24427  umgraex  24444  disjiunel  27585  qtophaus  27993  qqhval2  28116  esummono  28202  gsumesum  28207  measvuni  28341  fiunelcarsg  28443  carsgclctunlem1  28444  sitgclg  28467  eulerpartlemsv2  28480  eulerpartlemsv3  28483  eulerpartlemgc  28484  eulerpartlemv  28486  signstfvneq0  28712  signstfvcl  28713  signstfveq0a  28716  signstfveq0  28717  signsvfn  28722  signsvtp  28723  signsvtn  28724  signsvfpn  28725  signsvfnn  28726  signlem0  28727  dmgmn0  28757  dmgmaddnn0  28758  dmgmdivn0  28759  lgamgulmlem2  28761  lgamgulmlem3  28762  lgamgulmlem5  28764  lgamgulmlem6  28765  lgamgulm2  28767  lgambdd  28768  lgamucov  28769  lgamcvg2  28786  gamcvg  28787  gamcvg2lem  28790  iprodgam  29291  rrndstprj2  30493  qirropth  31009  rmxyneg  31021  rmxm1  31035  rmxluc  31037  rmxdbl  31040  ltrmxnn0  31052  jm2.19lem1  31097  jm2.23  31104  rmxdiophlem  31123  aomclem2  31167  bccm1k  31415  dstregt0  31630  fprodexp  31766  fprodabs2  31768  mccllem  31771  climrec  31775  climdivf  31784  islpcn  31811  lptre2pt  31812  0ellimcdiv  31821  reclimc  31825  divlimc  31828  divcncf  31852  cncficcgt0  31857  dvmptdiv  31880  dvdivf  31885  stoweidlem34  31982  stoweidlem43  31991  etransclem46  32229  etransclem47  32230  etransclem48  32231  uhgss  32687  zrzeroorngc  33010  zrtermoringc  33078  zrninitoringc  33079  nzerooringczr  33080  lsatelbN  35144  lsatfixedN  35147  lkreqN  35308  lkrlspeqN  35309  dochnel2  37532  dochnel  37533  djhcvat42  37555  dochsnshp  37593  dochexmidat  37599  dochsnkr  37612  dochsnkr2  37613  dochsnkr2cl  37614  dochflcl  37615  dochfl1  37616  dochfln0  37617  lcfl6lem  37638  lcfl7lem  37639  lcfl8b  37644  lclkrlem2a  37647  lclkrlem2b  37648  lclkrlem2c  37649  lclkrlem2d  37650  lclkrlem2e  37651  lclkrlem2f  37652  lcfrlem14  37696  lcfrlem15  37697  lcfrlem16  37698  lcfrlem17  37699  lcfrlem18  37700  lcfrlem19  37701  lcfrlem20  37702  lcfrlem21  37703  lcfrlem23  37705  lcfrlem25  37707  lcfrlem26  37708  lcfrlem35  37717  lcfrlem36  37718  mapdn0  37809  mapdpglem29  37840  mapdpglem24  37844  baerlem3lem1  37847  baerlem5alem1  37848  baerlem5blem1  37849  baerlem3lem2  37850  baerlem5alem2  37851  baerlem5blem2  37852  baerlem5amN  37856  baerlem5bmN  37857  baerlem5abmN  37858  mapdindp0  37859  mapdindp1  37860  mapdindp2  37861  mapdindp3  37862  mapdindp4  37863  mapdheq2  37869  mapdheq4lem  37871  mapdheq4  37872  mapdh6lem1N  37873  mapdh6lem2N  37874  mapdh6aN  37875  mapdh6bN  37877  mapdh6cN  37878  mapdh6dN  37879  mapdh6eN  37880  mapdh6fN  37881  mapdh6gN  37882  mapdh6hN  37883  mapdh6iN  37884  mapdh7eN  37888  mapdh7cN  37889  mapdh7dN  37890  mapdh7fN  37891  mapdh75e  37892  mapdh75fN  37895  hvmaplfl  37907  mapdhvmap  37909  mapdh8aa  37916  mapdh8ab  37917  mapdh8ad  37919  mapdh8b  37920  mapdh8c  37921  mapdh8d0N  37922  mapdh8d  37923  mapdh8e  37924  mapdh9a  37930  mapdh9aOLDN  37931  hdmap1val2  37941  hdmap1eq  37942  hdmap1valc  37944  hdmap1eq2  37946  hdmap1eq4N  37947  hdmap1l6lem1  37948  hdmap1l6lem2  37949  hdmap1l6a  37950  hdmap1l6b  37952  hdmap1l6c  37953  hdmap1l6d  37954  hdmap1l6e  37955  hdmap1l6f  37956  hdmap1l6g  37957  hdmap1l6h  37958  hdmap1l6i  37959  hdmap1eulem  37964  hdmap1eulemOLDN  37965  hdmap1neglem1N  37968  hdmapcl  37973  hdmapval2lem  37974  hdmapval0  37976  hdmapeveclem  37977  hdmapevec  37978  hdmapval3lemN  37980  hdmapval3N  37981  hdmap10lem  37982  hdmap11lem1  37984  hdmap11lem2  37985  hdmapnzcl  37988  hdmaprnlem3N  37993  hdmaprnlem3uN  37994  hdmaprnlem4N  37996  hdmaprnlem7N  37998  hdmaprnlem8N  37999  hdmaprnlem9N  38000  hdmaprnlem3eN  38001  hdmaprnlem16N  38005  hdmap14lem1  38011  hdmap14lem2N  38012  hdmap14lem3  38013  hdmap14lem4a  38014  hdmap14lem6  38016  hdmap14lem8  38018  hdmap14lem9  38019  hdmap14lem10  38020  hdmap14lem11  38021  hdmap14lem12  38022  hgmaprnlem1N  38039  hgmaprnlem2N  38040  hgmaprnlem3N  38041  hgmaprnlem4N  38042  hdmapip1  38059  hdmapinvlem1  38061  hdmapinvlem2  38062  hdmapinvlem3  38063  hdmapinvlem4  38064  hdmapglem5  38065  hgmapvvlem1  38066  hgmapvvlem2  38067  hgmapvvlem3  38068  hdmapglem7a  38070  hdmapglem7b  38071  hdmapglem7  38072
  Copyright terms: Public domain W3C validator