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

Theorem eldifad 3473
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3471. (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 3471 . . 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 1804    \ cdif 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464
This theorem is referenced by:  xpdifid  5425  unblem1  7774  cantnflem3  8113  cantnflem4  8114  cantnflem3OLD  8135  cantnflem4OLD  8136  oef1o  8144  oef1oOLD  8145  infxpenc  8398  infxpencOLD  8403  acndom2  8438  ackbij1lem18  8620  infpssrlem3  8688  fin23lem26  8708  fin23lem30  8725  pwfseqlem4a  9042  expclz  12173  symgextf  16421  pmtrfinv  16465  symggen  16474  efgsdmi  16729  efgs1b  16733  efgsp1  16734  efgsres  16735  efgredlemf  16738  efgredlemd  16741  efgredlem  16744  efgrelexlemb  16747  gsum2d2lem  16980  pgpfac1lem2  17105  pgpfac1lem3a  17106  pgpfac1lem3  17107  pgpfac1lem4  17108  isdrng2  17385  lvecinv  17738  lspsncmp  17741  lspsnne1  17742  lspsnnecom  17744  lspabs2  17745  lspsneu  17748  lspdisjb  17751  lspexch  17754  lspindp1  17758  lvecindp2  17764  lspsolv  17768  lspsnat  17770  lsppratlem1  17772  lsppratlem2  17773  fidomndrnglem  17934  frlmssuvc2  18804  frlmssuvc2OLD  18806  maducoeval2  19120  hauscmplem  19884  1stccnp  19941  imasdsf1olem  20854  rrxmetlem  21812  dvrec  22336  ftc1lem6  22420  elqaalem1  22693  elqaalem3  22695  ulmdvlem3  22775  abelthlem6  22809  abelthlem7a  22810  abelthlem7  22811  logtayl  23019  ftalem3  23326  lgsqrlem1  23594  lgsqrlem2  23595  lgsqrlem3  23596  lgsqrlem4  23597  lgseisenlem1  23602  lgseisenlem2  23603  lgseisenlem3  23604  lgseisenlem4  23605  lgseisen  23606  lgsquadlem2  23608  lgsquadlem3  23609  chebbnd1lem1  23632  dchrisum0re  23676  dchrisum0lema  23677  dchrisum0lem1b  23678  dchrisum0lem1  23679  dchrisum0lem2a  23680  dchrisum0lem2  23681  tgisline  23985  elntg  24265  uhgrass  24284  umgraex  24301  qtophaus  27817  qqhval2  27941  esummono  28044  gsumesum  28045  measvuni  28163  sitgclg  28262  eulerpartlemsv2  28275  eulerpartlemsv3  28278  eulerpartlemgc  28279  eulerpartlemv  28281  signstfvneq0  28507  signstfvcl  28508  signstfveq0a  28511  signstfveq0  28512  signsvfn  28517  signsvtp  28518  signsvtn  28519  signsvfpn  28520  signsvfnn  28521  signlem0  28522  dmgmn0  28546  dmgmaddnn0  28547  dmgmdivn0  28548  lgamgulmlem2  28550  lgamgulmlem3  28551  lgamgulmlem5  28553  lgamgulmlem6  28554  lgamgulm2  28556  lgambdd  28557  lgamucov  28558  lgamcvg2  28575  gamcvg  28576  gamcvg2lem  28579  iprodgam  29101  rrndstprj2  30303  qirropth  30820  rmxyneg  30832  rmxm1  30846  rmxluc  30848  rmxdbl  30851  ltrmxnn0  30863  jm2.19lem1  30907  jm2.23  30914  rmxdiophlem  30933  aomclem2  30977  dstregt0  31417  fprodexp  31554  fprodabs2  31556  mccllem  31559  climrec  31563  climdivf  31572  islpcn  31599  lptre2pt  31600  0ellimcdiv  31609  reclimc  31613  divlimc  31616  divcncf  31640  cncficcgt0  31645  dvmptdiv  31668  dvdivf  31673  stoweidlem34  31770  stoweidlem43  31779  etransclem46  32017  etransclem47  32018  etransclem48  32019  uhgss  32323  lsatelbN  34606  lsatfixedN  34609  lkreqN  34770  lkrlspeqN  34771  dochnel2  36994  dochnel  36995  djhcvat42  37017  dochsnshp  37055  dochexmidat  37061  dochsnkr  37074  dochsnkr2  37075  dochsnkr2cl  37076  dochflcl  37077  dochfl1  37078  dochfln0  37079  lcfl6lem  37100  lcfl7lem  37101  lcfl8b  37106  lclkrlem2a  37109  lclkrlem2b  37110  lclkrlem2c  37111  lclkrlem2d  37112  lclkrlem2e  37113  lclkrlem2f  37114  lcfrlem14  37158  lcfrlem15  37159  lcfrlem16  37160  lcfrlem17  37161  lcfrlem18  37162  lcfrlem19  37163  lcfrlem20  37164  lcfrlem21  37165  lcfrlem23  37167  lcfrlem25  37169  lcfrlem26  37170  lcfrlem35  37179  lcfrlem36  37180  mapdn0  37271  mapdpglem29  37302  mapdpglem24  37306  baerlem3lem1  37309  baerlem5alem1  37310  baerlem5blem1  37311  baerlem3lem2  37312  baerlem5alem2  37313  baerlem5blem2  37314  baerlem5amN  37318  baerlem5bmN  37319  baerlem5abmN  37320  mapdindp0  37321  mapdindp1  37322  mapdindp2  37323  mapdindp3  37324  mapdindp4  37325  mapdheq2  37331  mapdheq4lem  37333  mapdheq4  37334  mapdh6lem1N  37335  mapdh6lem2N  37336  mapdh6aN  37337  mapdh6bN  37339  mapdh6cN  37340  mapdh6dN  37341  mapdh6eN  37342  mapdh6fN  37343  mapdh6gN  37344  mapdh6hN  37345  mapdh6iN  37346  mapdh7eN  37350  mapdh7cN  37351  mapdh7dN  37352  mapdh7fN  37353  mapdh75e  37354  mapdh75fN  37357  hvmaplfl  37369  mapdhvmap  37371  mapdh8aa  37378  mapdh8ab  37379  mapdh8ad  37381  mapdh8b  37382  mapdh8c  37383  mapdh8d0N  37384  mapdh8d  37385  mapdh8e  37386  mapdh9a  37392  mapdh9aOLDN  37393  hdmap1val2  37403  hdmap1eq  37404  hdmap1valc  37406  hdmap1eq2  37408  hdmap1eq4N  37409  hdmap1l6lem1  37410  hdmap1l6lem2  37411  hdmap1l6a  37412  hdmap1l6b  37414  hdmap1l6c  37415  hdmap1l6d  37416  hdmap1l6e  37417  hdmap1l6f  37418  hdmap1l6g  37419  hdmap1l6h  37420  hdmap1l6i  37421  hdmap1eulem  37426  hdmap1eulemOLDN  37427  hdmap1neglem1N  37430  hdmapcl  37435  hdmapval2lem  37436  hdmapval0  37438  hdmapeveclem  37439  hdmapevec  37440  hdmapval3lemN  37442  hdmapval3N  37443  hdmap10lem  37444  hdmap11lem1  37446  hdmap11lem2  37447  hdmapnzcl  37450  hdmaprnlem3N  37455  hdmaprnlem3uN  37456  hdmaprnlem4N  37458  hdmaprnlem7N  37460  hdmaprnlem8N  37461  hdmaprnlem9N  37462  hdmaprnlem3eN  37463  hdmaprnlem16N  37467  hdmap14lem1  37473  hdmap14lem2N  37474  hdmap14lem3  37475  hdmap14lem4a  37476  hdmap14lem6  37478  hdmap14lem8  37480  hdmap14lem9  37481  hdmap14lem10  37482  hdmap14lem11  37483  hdmap14lem12  37484  hgmaprnlem1N  37501  hgmaprnlem2N  37502  hgmaprnlem3N  37503  hgmaprnlem4N  37504  hdmapip1  37521  hdmapinvlem1  37523  hdmapinvlem2  37524  hdmapinvlem3  37525  hdmapinvlem4  37526  hdmapglem5  37527  hgmapvvlem1  37528  hgmapvvlem2  37529  hgmapvvlem3  37530  hdmapglem7a  37532  hdmapglem7b  37533  hdmapglem7  37534
  Copyright terms: Public domain W3C validator