Theorem eldifad 3916

Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3914. (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 3914	. . 3 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
3	1, 2	sylib 220	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	3	simpld 498	1 ⊢ (𝜑 → 𝐴 ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2142   ∖ cdif 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907

This theorem is referenced by:  xpdifid  6153  xpdifcnvepel  6154  fvdifsupp  8151  unblem1  9236  cantnflem3  9646  cantnflem4  9647  oef1o  9653  infxpenc  9974  acndom2  10010  ackbij1lem18  10192  infpssrlem3  10262  fin23lem26  10282  fin23lem30  10299  pwfseqlem4a  10619  elfzodif0  13776  expclz  14097  pfxchn  18642  chnind  18653  chnccats1  18657  chnccat  18658  symgextf  19457  pmtrfinv  19501  symggen  19510  efgsdmi  19772  efgs1b  19776  efgsp1  19777  efgsres  19778  efgredlemf  19781  efgredlemd  19784  efgredlemc  19785  efgredlem  19787  efgrelexlemb  19790  gsum2d2lem  20013  pgpfac1lem2  20117  pgpfac1lem3a  20118  pgpfac1lem3  20119  pgpfac1lem4  20120  zrzeroorngc  20694  zrtermoringc  20725  zrninitoringc  20726  domneq0r  20774  isdrng2  20793  fidomndrnglem  20822  lvecinv  21183  lspsncmp  21186  lspsnne1  21187  lspsnnecom  21189  lspabs2  21190  lspsneu  21193  lspdisjb  21196  lspexch  21199  lspindp1  21203  lvecindp2  21209  lspsolv  21213  lspsnat  21215  lsppratlem1  21217  lsppratlem2  21218  nzerooringczr  21532  frlmssuvc2  21847  evls1fpws  22432  maducoeval2  22700  hauscmplem  23466  1stccnp  23522  imasdsf1olem  24433  rrxmetlem  25469  divcncf  25509  dvrec  26017  dvmptdiv  26036  ftc1lem6  26103  elqaalem1  26383  elqaalem3  26385  ulmdvlem3  26465  abelthlem6  26499  abelthlem7a  26500  abelthlem7  26501  logtayl  26725  dmgmn0  27090  dmgmaddnn0  27091  dmgmdivn0  27092  lgamgulmlem2  27094  lgamgulmlem3  27095  lgamgulmlem5  27097  lgamgulmlem6  27098  lgamgulm2  27100  lgambdd  27101  lgamucov  27102  lgamcvg2  27119  gamcvg  27120  gamcvg2lem  27123  ftalem3  27139  lgsqrlem1  27410  lgsqrlem2  27411  lgsqrlem3  27412  lgsqrlem4  27413  lgseisenlem1  27439  lgseisenlem2  27440  lgseisenlem3  27441  lgseisenlem4  27442  lgseisen  27443  lgsquadlem1  27444  lgsquadlem2  27445  lgsquadlem3  27446  chebbnd1lem1  27533  dchrisum0re  27577  dchrisum0lema  27578  dchrisum0lem1b  27579  dchrisum0lem1  27580  dchrisum0lem2a  27581  dchrisum0lem2  27582  tgisline  28796  tgelrnpln  28983  elplng  28987  elplngid  28989  plngcplem  28992  plngrotlem1  28994  plngrotlem2  28995  plngrotlem3  28996  plngrot  28997  lnssplnglem  28998  lnssplng  28999  elntg  29185  uhgrss  29265  upgrex  29293  edguhgr  29330  1loopgrvd0  29705  disjiunel  32796  suppovss  32883  nn0difffzod  33006  gsumfs2d  33241  gsumhashmul  33247  suppgsumssiun  33252  odpmco  33266  pmtrcnel  33269  pmtrcnelor  33271  cycpmco2f1  33304  cycpmco2rn  33305  cycpmco2lem1  33306  cycpmco2lem2  33307  cycpmco2lem3  33308  cycpmco2lem4  33309  cycpmco2lem5  33310  cycpmco2lem6  33311  cycpmco2lem7  33312  cycpmco2  33313  cyc3co2  33320  tocyccntz  33324  cyc3conja  33337  fxpsdrg  33355  elrgspnlem2  33424  elrgspnlem4  33426  elrgspnsubrunlem2  33429  domnprodn0  33459  domnprodeq0  33460  idomrcanOLD  33466  isdrng4  33482  fracfld  33495  lindssn  33564  lindfpropd  33568  elrspunidl  33614  elrspunsn  33615  drngidl  33619  prmidlsubm  33646  mxidlmaxv  33656  mxidlirredi  33659  opprqusdrng  33681  qsdrnglem2  33684  dflringlem  33690  dflringlem2  33691  rprmcl  33714  rprmirred  33727  pidufd  33739  1arithufdlem3  33742  dfufd2  33746  zringfrac  33750  deg1prod  33779  ply1dg3rt0irred  33780  gsummoncoe1fzo  33793  mplvrpmrhm  33844  psrgsum  33845  psrmonprod  33849  esplyfval2  33862  lindsunlem  33921  fedgmullem1  33926  fedgmullem2  33927  assafld  33934  fldextrspunlsp  33971  extdgfialglem2  33990  irngnminplynz  34009  constrextdg2lem  34045  constrfiss  34048  constrsdrg  34072  submatminr1  34107  qtophaus  34133  qqhval2  34279  esummono  34351  gsumesum  34356  esum2dlem  34389  measvuni  34511  fiunelcarsg  34613  sitgclg  34639  sitgaddlemb  34645  eulerpartlemsv2  34655  eulerpartlemsv3  34658  eulerpartlemgc  34659  eulerpartlemv  34661  signstfvneq0  34866  signstfvcl  34867  signstfveq0a  34870  signstfveq0  34871  signsvfn  34876  signsvtp  34877  signsvtn  34878  signsvfpn  34879  signsvfnn  34880  signlem0  34881  hgt750leme  34952  onvf1odlem4  35449  iprodgam  36092  ttcwf2  36885  mh-inf3f1  36901  poimirlem2  38121  rrndstprj2  38330  lsatelbN  39630  lsatfixedN  39633  lkreqN  39794  lkrlspeqN  39795  dochnel2  42016  dochnel  42017  djhcvat42  42039  dochsnshp  42077  dochexmidat  42083  dochsnkr  42096  dochsnkr2  42097  dochsnkr2cl  42098  dochflcl  42099  dochfl1  42100  dochfln0  42101  lcfl6lem  42122  lcfl7lem  42123  lcfl8b  42128  lclkrlem2a  42131  lclkrlem2b  42132  lclkrlem2c  42133  lclkrlem2d  42134  lclkrlem2e  42135  lclkrlem2f  42136  lcfrlem14  42180  lcfrlem15  42181  lcfrlem16  42182  lcfrlem17  42183  lcfrlem18  42184  lcfrlem19  42185  lcfrlem20  42186  lcfrlem21  42187  lcfrlem23  42189  lcfrlem25  42191  lcfrlem26  42192  lcfrlem35  42201  lcfrlem36  42202  mapdn0  42293  mapdpglem29  42324  mapdpglem24  42328  baerlem3lem1  42331  baerlem5alem1  42332  baerlem5blem1  42333  baerlem3lem2  42334  baerlem5alem2  42335  baerlem5blem2  42336  baerlem5amN  42340  baerlem5bmN  42341  baerlem5abmN  42342  mapdindp0  42343  mapdindp1  42344  mapdindp2  42345  mapdindp3  42346  mapdindp4  42347  mapdheq2  42353  mapdheq4lem  42355  mapdheq4  42356  mapdh6lem1N  42357  mapdh6lem2N  42358  mapdh6aN  42359  mapdh6bN  42361  mapdh6cN  42362  mapdh6dN  42363  mapdh6eN  42364  mapdh6fN  42365  mapdh6gN  42366  mapdh6hN  42367  mapdh6iN  42368  mapdh7eN  42372  mapdh7cN  42373  mapdh7dN  42374  mapdh7fN  42375  mapdh75e  42376  mapdh75fN  42379  hvmaplfl  42391  mapdhvmap  42393  mapdh8aa  42400  mapdh8ab  42401  mapdh8ad  42403  mapdh8b  42404  mapdh8c  42405  mapdh8d0N  42406  mapdh8d  42407  mapdh8e  42408  mapdh9a  42413  mapdh9aOLDN  42414  hdmap1val2  42424  hdmap1eq  42425  hdmap1valc  42427  hdmap1eq2  42429  hdmap1eq4N  42430  hdmap1l6lem1  42431  hdmap1l6lem2  42432  hdmap1l6a  42433  hdmap1l6b  42435  hdmap1l6c  42436  hdmap1l6d  42437  hdmap1l6e  42438  hdmap1l6f  42439  hdmap1l6g  42440  hdmap1l6h  42441  hdmap1l6i  42442  hdmap1eulem  42446  hdmap1eulemOLDN  42447  hdmapcl  42454  hdmapval2lem  42455  hdmapval0  42457  hdmapeveclem  42458  hdmapevec  42459  hdmapval3lemN  42461  hdmapval3N  42462  hdmap10lem  42463  hdmap11lem1  42465  hdmap11lem2  42466  hdmapnzcl  42469  hdmaprnlem3N  42474  hdmaprnlem3uN  42475  hdmaprnlem4N  42477  hdmaprnlem7N  42479  hdmaprnlem8N  42480  hdmaprnlem9N  42481  hdmaprnlem3eN  42482  hdmaprnlem16N  42486  hdmap14lem1  42492  hdmap14lem2N  42493  hdmap14lem3  42494  hdmap14lem4a  42495  hdmap14lem6  42497  hdmap14lem8  42499  hdmap14lem9  42500  hdmap14lem10  42501  hdmap14lem11  42502  hdmap14lem12  42503  hgmaprnlem1N  42520  hgmaprnlem2N  42521  hgmaprnlem3N  42522  hgmaprnlem4N  42523  hdmapip1  42540  hdmapinvlem1  42542  hdmapinvlem2  42543  hdmapinvlem3  42544  hdmapinvlem4  42545  hdmapglem5  42546  hgmapvvlem1  42547  hgmapvvlem2  42548  hgmapvvlem3  42549  hdmapglem7a  42551  hdmapglem7b  42552  hdmapglem7  42553  evl1gprodd  42734  nelsubginvcld  43118  nelsubgcld  43119  nelsubgsubcld  43120  domnexpgn0cl  43141  fidomncyc  43153  prjspnfv01  43206  prjspner01  43207  prjspner1  43208  dffltz  43216  qirropth  43485  rmxyneg  43497  rmxm1  43511  rmxluc  43513  rmxdbl  43516  ltrmxnn0  43526  jm2.19lem1  43566  jm2.23  43573  rmxdiophlem  43592  aomclem2  43632  cantnftermord  43897  inaex  44873  bccm1k  44918  dstregt0  45861  fprodexp  46170  fprodabs2  46171  mccllem  46173  fprodcnlem  46175  climrec  46179  climdivf  46188  islpcn  46213  lptre2pt  46214  0ellimcdiv  46223  reclimc  46227  divlimc  46230  cncficcgt0  46462  dvdivf  46496  stoweidlem34  46608  stoweidlem43  46617  etransclem46  46854  etransclem47  46855  etransclem48  46856  hsphoidmvle2  47159  hsphoidmvle  47160  hoidmvlelem3  47171  hoidmvlelem4  47172  hspdifhsp  47190  readdcnnred  47897  resubcnnred  47898  recnmulnred  47899  cndivrenred  47900