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

Theorem eldifad 3418
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3416. (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 3416 . . 3  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
31, 2sylib 200 . 2  |-  ( ph  ->  ( A  e.  B  /\  -.  A  e.  C
) )
43simpld 461 1  |-  ( ph  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 371    e. wcel 1889    \ cdif 3403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-dif 3409
This theorem is referenced by:  xpdifid  5268  unblem1  7828  cantnflem3  8201  cantnflem4  8202  oef1o  8208  infxpenc  8454  acndom2  8490  ackbij1lem18  8672  infpssrlem3  8740  fin23lem26  8760  fin23lem30  8777  pwfseqlem4a  9091  expclz  12304  symgextf  17070  pmtrfinv  17114  symggen  17123  efgsdmi  17394  efgs1b  17398  efgsp1  17399  efgsres  17400  efgredlemf  17403  efgredlemd  17406  efgredlem  17409  efgrelexlemb  17412  gsum2d2lem  17617  pgpfac1lem2  17720  pgpfac1lem3a  17721  pgpfac1lem3  17722  pgpfac1lem4  17723  isdrng2  17997  lvecinv  18348  lspsncmp  18351  lspsnne1  18352  lspsnnecom  18354  lspabs2  18355  lspsneu  18358  lspdisjb  18361  lspexch  18364  lspindp1  18368  lvecindp2  18374  lspsolv  18378  lspsnat  18380  lsppratlem1  18382  lsppratlem2  18383  fidomndrnglem  18542  frlmssuvc2  19365  maducoeval2  19677  hauscmplem  20433  1stccnp  20489  imasdsf1olem  21400  rrxmetlem  22373  dvrec  22921  ftc1lem6  23005  elqaalem1  23284  elqaalem3  23286  elqaalem1OLD  23287  elqaalem3OLD  23289  ulmdvlem3  23369  abelthlem6  23403  abelthlem7a  23404  abelthlem7  23405  logtayl  23617  dmgmn0  23963  dmgmaddnn0  23964  dmgmdivn0  23965  lgamgulmlem2  23967  lgamgulmlem3  23968  lgamgulmlem5  23970  lgamgulmlem6  23971  lgamgulm2  23973  lgambdd  23974  lgamucov  23975  lgamcvg2  23992  gamcvg  23993  gamcvg2lem  23996  ftalem3  24011  lgsqrlem1  24281  lgsqrlem2  24282  lgsqrlem3  24283  lgsqrlem4  24284  lgseisenlem1  24289  lgseisenlem2  24290  lgseisenlem3  24291  lgseisenlem4  24292  lgseisen  24293  lgsquadlem2  24295  lgsquadlem3  24296  chebbnd1lem1  24319  dchrisum0re  24363  dchrisum0lema  24364  dchrisum0lem1b  24365  dchrisum0lem1  24366  dchrisum0lem2a  24367  dchrisum0lem2  24368  tgisline  24684  elntg  25026  uhgrass  25045  umgraex  25062  disjiunel  28218  submatminr1  28648  qtophaus  28675  qqhval2  28798  esummono  28887  gsumesum  28892  measvuni  29048  fiunelcarsg  29160  carsgclctunlem1  29161  sitgclg  29187  sitgaddlemb  29193  eulerpartlemsv2  29203  eulerpartlemsv3  29206  eulerpartlemgc  29207  eulerpartlemv  29209  signstfvneq0  29473  signstfvcl  29474  signstfveq0a  29477  signstfveq0  29478  signsvfn  29483  signsvtp  29484  signsvtn  29485  signsvfpn  29486  signsvfnn  29487  signlem0  29488  iprodgam  30390  poimirlem2  31954  rrndstprj2  32175  lsatelbN  32584  lsatfixedN  32587  lkreqN  32748  lkrlspeqN  32749  dochnel2  34972  dochnel  34973  djhcvat42  34995  dochsnshp  35033  dochexmidat  35039  dochsnkr  35052  dochsnkr2  35053  dochsnkr2cl  35054  dochflcl  35055  dochfl1  35056  dochfln0  35057  lcfl6lem  35078  lcfl7lem  35079  lcfl8b  35084  lclkrlem2a  35087  lclkrlem2b  35088  lclkrlem2c  35089  lclkrlem2d  35090  lclkrlem2e  35091  lclkrlem2f  35092  lcfrlem14  35136  lcfrlem15  35137  lcfrlem16  35138  lcfrlem17  35139  lcfrlem18  35140  lcfrlem19  35141  lcfrlem20  35142  lcfrlem21  35143  lcfrlem23  35145  lcfrlem25  35147  lcfrlem26  35148  lcfrlem35  35157  lcfrlem36  35158  mapdn0  35249  mapdpglem29  35280  mapdpglem24  35284  baerlem3lem1  35287  baerlem5alem1  35288  baerlem5blem1  35289  baerlem3lem2  35290  baerlem5alem2  35291  baerlem5blem2  35292  baerlem5amN  35296  baerlem5bmN  35297  baerlem5abmN  35298  mapdindp0  35299  mapdindp1  35300  mapdindp2  35301  mapdindp3  35302  mapdindp4  35303  mapdheq2  35309  mapdheq4lem  35311  mapdheq4  35312  mapdh6lem1N  35313  mapdh6lem2N  35314  mapdh6aN  35315  mapdh6bN  35317  mapdh6cN  35318  mapdh6dN  35319  mapdh6eN  35320  mapdh6fN  35321  mapdh6gN  35322  mapdh6hN  35323  mapdh6iN  35324  mapdh7eN  35328  mapdh7cN  35329  mapdh7dN  35330  mapdh7fN  35331  mapdh75e  35332  mapdh75fN  35335  hvmaplfl  35347  mapdhvmap  35349  mapdh8aa  35356  mapdh8ab  35357  mapdh8ad  35359  mapdh8b  35360  mapdh8c  35361  mapdh8d0N  35362  mapdh8d  35363  mapdh8e  35364  mapdh9a  35370  mapdh9aOLDN  35371  hdmap1val2  35381  hdmap1eq  35382  hdmap1valc  35384  hdmap1eq2  35386  hdmap1eq4N  35387  hdmap1l6lem1  35388  hdmap1l6lem2  35389  hdmap1l6a  35390  hdmap1l6b  35392  hdmap1l6c  35393  hdmap1l6d  35394  hdmap1l6e  35395  hdmap1l6f  35396  hdmap1l6g  35397  hdmap1l6h  35398  hdmap1l6i  35399  hdmap1eulem  35404  hdmap1eulemOLDN  35405  hdmap1neglem1N  35408  hdmapcl  35413  hdmapval2lem  35414  hdmapval0  35416  hdmapeveclem  35417  hdmapevec  35418  hdmapval3lemN  35420  hdmapval3N  35421  hdmap10lem  35422  hdmap11lem1  35424  hdmap11lem2  35425  hdmapnzcl  35428  hdmaprnlem3N  35433  hdmaprnlem3uN  35434  hdmaprnlem4N  35436  hdmaprnlem7N  35438  hdmaprnlem8N  35439  hdmaprnlem9N  35440  hdmaprnlem3eN  35441  hdmaprnlem16N  35445  hdmap14lem1  35451  hdmap14lem2N  35452  hdmap14lem3  35453  hdmap14lem4a  35454  hdmap14lem6  35456  hdmap14lem8  35458  hdmap14lem9  35459  hdmap14lem10  35460  hdmap14lem11  35461  hdmap14lem12  35462  hgmaprnlem1N  35479  hgmaprnlem2N  35480  hgmaprnlem3N  35481  hgmaprnlem4N  35482  hdmapip1  35499  hdmapinvlem1  35501  hdmapinvlem2  35502  hdmapinvlem3  35503  hdmapinvlem4  35504  hdmapglem5  35505  hgmapvvlem1  35506  hgmapvvlem2  35507  hgmapvvlem3  35508  hdmapglem7a  35510  hdmapglem7b  35511  hdmapglem7  35512  qirropth  35768  rmxyneg  35780  rmxm1  35794  rmxluc  35796  rmxdbl  35799  ltrmxnn0  35811  jm2.19lem1  35856  jm2.23  35863  rmxdiophlem  35882  aomclem2  35925  bccm1k  36702  dstregt0  37501  fprodexp  37684  fprodabs2  37685  mccllem  37687  climrec  37691  climdivf  37702  islpcn  37729  lptre2pt  37730  0ellimcdiv  37740  reclimc  37744  divlimc  37747  divcncf  37771  cncficcgt0  37776  dvmptdiv  37799  dvdivf  37804  stoweidlem34  37905  stoweidlem43  37914  etransclem46  38155  etransclem47  38156  etransclem48OLD  38157  etransclem48  38158  hsphoidmvle2  38417  hsphoidmvle  38418  hoidmvlelem3  38429  hoidmvlelem4  38430  hspdifhsp  38448  uhgrss  39165  upgrex  39194  edguhgr  39231  uhgssALTV  39785  zrzeroorngc  40108  zrtermoringc  40176  zrninitoringc  40177  nzerooringczr  40178
  Copyright terms: Public domain W3C validator