Theorem eldifad 3487

Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3485. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
eldifad.1

Assertion

Ref	Expression
eldifad

Proof of Theorem eldifad

Step	Hyp	Ref	Expression
1		eldifad.1	. . 3
2		eldif 3485	. . 3
3	1, 2	sylib 196	. 2
4	3	simpld 459	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369  e.wcel 1818  \cdif 3472

This theorem is referenced by:  xpdifid  5440  unblem1  7792  cantnflem3  8131  cantnflem4  8132  cantnflem3OLD  8153  cantnflem4OLD  8154  oef1o  8162  oef1oOLD  8163  infxpenc  8416  infxpencOLD  8421  acndom2  8456  ackbij1lem18  8638  infpssrlem3  8706  fin23lem26  8726  fin23lem30  8743  pwfseqlem4a  9060  expclz  12191  symgextf  16442  pmtrfinv  16486  symggen  16495  efgsdmi  16750  efgs1b  16754  efgsp1  16755  efgsres  16756  efgredlemf  16759  efgredlemd  16762  efgredlem  16765  efgrelexlemb  16768  gsum2d2lem  17001  pgpfac1lem2  17126  pgpfac1lem3a  17127  pgpfac1lem3  17128  pgpfac1lem4  17129  isdrng2  17406  lvecinv  17759  lspsncmp  17762  lspsnne1  17763  lspsnnecom  17765  lspabs2  17766  lspsneu  17769  lspdisjb  17772  lspexch  17775  lspindp1  17779  lvecindp2  17785  lspsolv  17789  lspsnat  17791  lsppratlem1  17793  lsppratlem2  17794  fidomndrnglem  17955  frlmssuvc2  18826  frlmssuvc2OLD  18828  maducoeval2  19142  hauscmplem  19906  1stccnp  19963  imasdsf1olem  20876  rrxmetlem  21834  dvrec  22358  ftc1lem6  22442  elqaalem1  22715  elqaalem3  22717  ulmdvlem3  22797  abelthlem6  22831  abelthlem7a  22832  abelthlem7  22833  logtayl  23041  ftalem3  23348  lgsqrlem1  23616  lgsqrlem2  23617  lgsqrlem3  23618  lgsqrlem4  23619  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem3  23626  lgseisenlem4  23627  lgseisen  23628  lgsquadlem2  23630  lgsquadlem3  23631  chebbnd1lem1  23654  dchrisum0re  23698  dchrisum0lema  23699  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem2  23703  tgisline  24007  elntg  24287  uhgrass  24306  umgraex  24323  qtophaus  27839  qqhval2  27963  esummono  28066  gsumesum  28067  measvuni  28185  sitgclg  28284  eulerpartlemsv2  28297  eulerpartlemsv3  28300  eulerpartlemgc  28301  eulerpartlemv  28303  signstfvneq0  28529  signstfvcl  28530  signstfveq0a  28533  signstfveq0  28534  signsvfn  28539  signsvtp  28540  signsvtn  28541  signsvfpn  28542  signsvfnn  28543  signlem0  28544  dmgmn0  28568  dmgmaddnn0  28569  dmgmdivn0  28570  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem5  28575  lgamgulmlem6  28576  lgamgulm2  28578  lgambdd  28579  lgamucov  28580  lgamcvg2  28597  gamcvg  28598  gamcvg2lem  28601  iprodgam  29125  rrndstprj2  30327  qirropth  30844  rmxyneg  30856  rmxm1  30870  rmxluc  30872  rmxdbl  30875  ltrmxnn0  30887  jm2.19lem1  30931  jm2.23  30938  rmxdiophlem  30957  aomclem2  31001  bccm1k  31247  dstregt0  31463  fprodexp  31600  fprodabs2  31602  mccllem  31605  climrec  31609  climdivf  31618  islpcn  31645  lptre2pt  31646  0ellimcdiv  31655  reclimc  31659  divlimc  31662  divcncf  31686  cncficcgt0  31691  dvmptdiv  31714  dvdivf  31719  stoweidlem34  31816  stoweidlem43  31825  etransclem46  32063  etransclem47  32064  etransclem48  32065  uhgss  32369  zrzeroorngc  32810  zrtermoringc  32878  zrninitoringc  32879  nzerooringczr  32880  lsatelbN  34731  lsatfixedN  34734  lkreqN  34895  lkrlspeqN  34896  dochnel2  37119  dochnel  37120  djhcvat42  37142  dochsnshp  37180  dochexmidat  37186  dochsnkr  37199  dochsnkr2  37200  dochsnkr2cl  37201  dochflcl  37202  dochfl1  37203  dochfln0  37204  lcfl6lem  37225  lcfl7lem  37226  lcfl8b  37231  lclkrlem2a  37234  lclkrlem2b  37235  lclkrlem2c  37236  lclkrlem2d  37237  lclkrlem2e  37238  lclkrlem2f  37239  lcfrlem14  37283  lcfrlem15  37284  lcfrlem16  37285  lcfrlem17  37286  lcfrlem18  37287  lcfrlem19  37288  lcfrlem20  37289  lcfrlem21  37290  lcfrlem23  37292  lcfrlem25  37294  lcfrlem26  37295  lcfrlem35  37304  lcfrlem36  37305  mapdn0  37396  mapdpglem29  37427  mapdpglem24  37431  baerlem3lem1  37434  baerlem5alem1  37435  baerlem5blem1  37436  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  baerlem5amN  37443  baerlem5bmN  37444  baerlem5abmN  37445  mapdindp0  37446  mapdindp1  37447  mapdindp2  37448  mapdindp3  37449  mapdindp4  37450  mapdheq2  37456  mapdheq4lem  37458  mapdheq4  37459  mapdh6lem1N  37460  mapdh6lem2N  37461  mapdh6aN  37462  mapdh6bN  37464  mapdh6cN  37465  mapdh6dN  37466  mapdh6eN  37467  mapdh6fN  37468  mapdh6gN  37469  mapdh6hN  37470  mapdh6iN  37471  mapdh7eN  37475  mapdh7cN  37476  mapdh7dN  37477  mapdh7fN  37478  mapdh75e  37479  mapdh75fN  37482  hvmaplfl  37494  mapdhvmap  37496  mapdh8aa  37503  mapdh8ab  37504  mapdh8ad  37506  mapdh8b  37507  mapdh8c  37508  mapdh8d0N  37509  mapdh8d  37510  mapdh8e  37511  mapdh9a  37517  mapdh9aOLDN  37518  hdmap1val2  37528  hdmap1eq  37529  hdmap1valc  37531  hdmap1eq2  37533  hdmap1eq4N  37534  hdmap1l6lem1  37535  hdmap1l6lem2  37536  hdmap1l6a  37537  hdmap1l6b  37539  hdmap1l6c  37540  hdmap1l6d  37541  hdmap1l6e  37542  hdmap1l6f  37543  hdmap1l6g  37544  hdmap1l6h  37545  hdmap1l6i  37546  hdmap1eulem  37551  hdmap1eulemOLDN  37552  hdmap1neglem1N  37555  hdmapcl  37560  hdmapval2lem  37561  hdmapval0  37563  hdmapeveclem  37564  hdmapevec  37565  hdmapval3lemN  37567  hdmapval3N  37568  hdmap10lem  37569  hdmap11lem1  37571  hdmap11lem2  37572  hdmapnzcl  37575  hdmaprnlem3N  37580  hdmaprnlem3uN  37581  hdmaprnlem4N  37583  hdmaprnlem7N  37585  hdmaprnlem8N  37586  hdmaprnlem9N  37587  hdmaprnlem3eN  37588  hdmaprnlem16N  37592  hdmap14lem1  37598  hdmap14lem2N  37599  hdmap14lem3  37600  hdmap14lem4a  37601  hdmap14lem6  37603  hdmap14lem8  37605  hdmap14lem9  37606  hdmap14lem10  37607  hdmap14lem11  37608  hdmap14lem12  37609  hgmaprnlem1N  37626  hgmaprnlem2N  37627  hgmaprnlem3N  37628  hgmaprnlem4N  37629  hdmapip1  37646  hdmapinvlem1  37648  hdmapinvlem2  37649  hdmapinvlem3  37650  hdmapinvlem4  37651  hdmapglem5  37652  hgmapvvlem1  37653  hgmapvvlem2  37654  hgmapvvlem3  37655  hdmapglem7a  37657  hdmapglem7b  37658  hdmapglem7  37659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478