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

Theorem eldifad 3402
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3400. (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 3400 . . 3  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
31, 2sylib 201 . 2  |-  ( ph  ->  ( A  e.  B  /\  -.  A  e.  C
) )
43simpld 466 1  |-  ( ph  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 376    e. wcel 1904    \ cdif 3387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-dif 3393
This theorem is referenced by:  xpdifid  5271  unblem1  7841  cantnflem3  8214  cantnflem4  8215  oef1o  8221  infxpenc  8467  acndom2  8503  ackbij1lem18  8685  infpssrlem3  8753  fin23lem26  8773  fin23lem30  8790  pwfseqlem4a  9104  expclz  12335  symgextf  17136  pmtrfinv  17180  symggen  17189  efgsdmi  17460  efgs1b  17464  efgsp1  17465  efgsres  17466  efgredlemf  17469  efgredlemd  17472  efgredlem  17475  efgrelexlemb  17478  gsum2d2lem  17683  pgpfac1lem2  17786  pgpfac1lem3a  17787  pgpfac1lem3  17788  pgpfac1lem4  17789  isdrng2  18063  lvecinv  18414  lspsncmp  18417  lspsnne1  18418  lspsnnecom  18420  lspabs2  18421  lspsneu  18424  lspdisjb  18427  lspexch  18430  lspindp1  18434  lvecindp2  18440  lspsolv  18444  lspsnat  18446  lsppratlem1  18448  lsppratlem2  18449  fidomndrnglem  18607  frlmssuvc2  19430  maducoeval2  19742  hauscmplem  20498  1stccnp  20554  imasdsf1olem  21466  rrxmetlem  22439  dvrec  22988  ftc1lem6  23072  elqaalem1  23351  elqaalem3  23353  elqaalem1OLD  23354  elqaalem3OLD  23356  ulmdvlem3  23436  abelthlem6  23470  abelthlem7a  23471  abelthlem7  23472  logtayl  23684  dmgmn0  24030  dmgmaddnn0  24031  dmgmdivn0  24032  lgamgulmlem2  24034  lgamgulmlem3  24035  lgamgulmlem5  24037  lgamgulmlem6  24038  lgamgulm2  24040  lgambdd  24041  lgamucov  24042  lgamcvg2  24059  gamcvg  24060  gamcvg2lem  24063  ftalem3  24078  lgsqrlem1  24348  lgsqrlem2  24349  lgsqrlem3  24350  lgsqrlem4  24351  lgseisenlem1  24356  lgseisenlem2  24357  lgseisenlem3  24358  lgseisenlem4  24359  lgseisen  24360  lgsquadlem2  24362  lgsquadlem3  24363  chebbnd1lem1  24386  dchrisum0re  24430  dchrisum0lema  24431  dchrisum0lem1b  24432  dchrisum0lem1  24433  dchrisum0lem2a  24434  dchrisum0lem2  24435  tgisline  24751  elntg  25093  uhgrass  25112  umgraex  25129  disjiunel  28283  submatminr1  28710  qtophaus  28737  qqhval2  28860  esummono  28949  gsumesum  28954  measvuni  29110  fiunelcarsg  29221  carsgclctunlem1  29222  sitgclg  29248  sitgaddlemb  29254  eulerpartlemsv2  29264  eulerpartlemsv3  29267  eulerpartlemgc  29268  eulerpartlemv  29270  signstfvneq0  29533  signstfvcl  29534  signstfveq0a  29537  signstfveq0  29538  signsvfn  29543  signsvtp  29544  signsvtn  29545  signsvfpn  29546  signsvfnn  29547  signlem0  29548  iprodgam  30449  poimirlem2  32006  rrndstprj2  32227  lsatelbN  32643  lsatfixedN  32646  lkreqN  32807  lkrlspeqN  32808  dochnel2  35031  dochnel  35032  djhcvat42  35054  dochsnshp  35092  dochexmidat  35098  dochsnkr  35111  dochsnkr2  35112  dochsnkr2cl  35113  dochflcl  35114  dochfl1  35115  dochfln0  35116  lcfl6lem  35137  lcfl7lem  35138  lcfl8b  35143  lclkrlem2a  35146  lclkrlem2b  35147  lclkrlem2c  35148  lclkrlem2d  35149  lclkrlem2e  35150  lclkrlem2f  35151  lcfrlem14  35195  lcfrlem15  35196  lcfrlem16  35197  lcfrlem17  35198  lcfrlem18  35199  lcfrlem19  35200  lcfrlem20  35201  lcfrlem21  35202  lcfrlem23  35204  lcfrlem25  35206  lcfrlem26  35207  lcfrlem35  35216  lcfrlem36  35217  mapdn0  35308  mapdpglem29  35339  mapdpglem24  35343  baerlem3lem1  35346  baerlem5alem1  35347  baerlem5blem1  35348  baerlem3lem2  35349  baerlem5alem2  35350  baerlem5blem2  35351  baerlem5amN  35355  baerlem5bmN  35356  baerlem5abmN  35357  mapdindp0  35358  mapdindp1  35359  mapdindp2  35360  mapdindp3  35361  mapdindp4  35362  mapdheq2  35368  mapdheq4lem  35370  mapdheq4  35371  mapdh6lem1N  35372  mapdh6lem2N  35373  mapdh6aN  35374  mapdh6bN  35376  mapdh6cN  35377  mapdh6dN  35378  mapdh6eN  35379  mapdh6fN  35380  mapdh6gN  35381  mapdh6hN  35382  mapdh6iN  35383  mapdh7eN  35387  mapdh7cN  35388  mapdh7dN  35389  mapdh7fN  35390  mapdh75e  35391  mapdh75fN  35394  hvmaplfl  35406  mapdhvmap  35408  mapdh8aa  35415  mapdh8ab  35416  mapdh8ad  35418  mapdh8b  35419  mapdh8c  35420  mapdh8d0N  35421  mapdh8d  35422  mapdh8e  35423  mapdh9a  35429  mapdh9aOLDN  35430  hdmap1val2  35440  hdmap1eq  35441  hdmap1valc  35443  hdmap1eq2  35445  hdmap1eq4N  35446  hdmap1l6lem1  35447  hdmap1l6lem2  35448  hdmap1l6a  35449  hdmap1l6b  35451  hdmap1l6c  35452  hdmap1l6d  35453  hdmap1l6e  35454  hdmap1l6f  35455  hdmap1l6g  35456  hdmap1l6h  35457  hdmap1l6i  35458  hdmap1eulem  35463  hdmap1eulemOLDN  35464  hdmap1neglem1N  35467  hdmapcl  35472  hdmapval2lem  35473  hdmapval0  35475  hdmapeveclem  35476  hdmapevec  35477  hdmapval3lemN  35479  hdmapval3N  35480  hdmap10lem  35481  hdmap11lem1  35483  hdmap11lem2  35484  hdmapnzcl  35487  hdmaprnlem3N  35492  hdmaprnlem3uN  35493  hdmaprnlem4N  35495  hdmaprnlem7N  35497  hdmaprnlem8N  35498  hdmaprnlem9N  35499  hdmaprnlem3eN  35500  hdmaprnlem16N  35504  hdmap14lem1  35510  hdmap14lem2N  35511  hdmap14lem3  35512  hdmap14lem4a  35513  hdmap14lem6  35515  hdmap14lem8  35517  hdmap14lem9  35518  hdmap14lem10  35519  hdmap14lem11  35520  hdmap14lem12  35521  hgmaprnlem1N  35538  hgmaprnlem2N  35539  hgmaprnlem3N  35540  hgmaprnlem4N  35541  hdmapip1  35558  hdmapinvlem1  35560  hdmapinvlem2  35561  hdmapinvlem3  35562  hdmapinvlem4  35563  hdmapglem5  35564  hgmapvvlem1  35565  hgmapvvlem2  35566  hgmapvvlem3  35567  hdmapglem7a  35569  hdmapglem7b  35570  hdmapglem7  35571  qirropth  35827  rmxyneg  35839  rmxm1  35853  rmxluc  35855  rmxdbl  35858  ltrmxnn0  35870  jm2.19lem1  35915  jm2.23  35922  rmxdiophlem  35941  aomclem2  35984  bccm1k  36761  dstregt0  37581  fprodexp  37771  fprodabs2  37772  mccllem  37774  climrec  37778  climdivf  37789  islpcn  37816  lptre2pt  37817  0ellimcdiv  37827  reclimc  37831  divlimc  37834  divcncf  37858  cncficcgt0  37863  dvmptdiv  37886  dvdivf  37891  stoweidlem34  38007  stoweidlem43  38016  etransclem46  38257  etransclem47  38258  etransclem48OLD  38259  etransclem48  38260  hsphoidmvle2  38525  hsphoidmvle  38526  hoidmvlelem3  38537  hoidmvlelem4  38538  hspdifhsp  38556  uhgrss  39308  upgrex  39338  edguhgr  39382  1loopgrvd0  39726  uhgssALTV  40189  zrzeroorngc  40512  zrtermoringc  40580  zrninitoringc  40581  nzerooringczr  40582
  Copyright terms: Public domain W3C validator