Theorem eldifad 3915

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2109   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906

This theorem is referenced by:  xpdifid  6117  fvdifsupp  8104  unblem1  9181  cantnflem3  9587  cantnflem4  9588  oef1o  9594  infxpenc  9912  acndom2  9948  ackbij1lem18  10130  infpssrlem3  10199  fin23lem26  10219  fin23lem30  10236  pwfseqlem4a  10555  expclz  13991  symgextf  19296  pmtrfinv  19340  symggen  19349  efgsdmi  19611  efgs1b  19615  efgsp1  19616  efgsres  19617  efgredlemf  19620  efgredlemd  19623  efgredlemc  19624  efgredlem  19626  efgrelexlemb  19629  gsum2d2lem  19852  pgpfac1lem2  19956  pgpfac1lem3a  19957  pgpfac1lem3  19958  pgpfac1lem4  19959  zrzeroorngc  20529  zrtermoringc  20560  zrninitoringc  20561  domneq0r  20609  isdrng2  20628  fidomndrnglem  20657  lvecinv  21020  lspsncmp  21023  lspsnne1  21024  lspsnnecom  21026  lspabs2  21027  lspsneu  21030  lspdisjb  21033  lspexch  21036  lspindp1  21040  lvecindp2  21046  lspsolv  21050  lspsnat  21052  lsppratlem1  21054  lsppratlem2  21055  nzerooringczr  21387  frlmssuvc2  21702  evls1fpws  22254  maducoeval2  22525  hauscmplem  23291  1stccnp  23347  imasdsf1olem  24259  rrxmetlem  25305  divcncf  25346  dvrec  25857  dvmptdiv  25876  ftc1lem6  25946  elqaalem1  26225  elqaalem3  26227  ulmdvlem3  26309  abelthlem6  26344  abelthlem7a  26345  abelthlem7  26346  logtayl  26567  dmgmn0  26934  dmgmaddnn0  26935  dmgmdivn0  26936  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamgulmlem5  26941  lgamgulmlem6  26942  lgamgulm2  26944  lgambdd  26945  lgamucov  26946  lgamcvg2  26963  gamcvg  26964  gamcvg2lem  26967  ftalem3  26983  lgsqrlem1  27255  lgsqrlem2  27256  lgsqrlem3  27257  lgsqrlem4  27258  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgseisenlem4  27287  lgseisen  27288  lgsquadlem1  27289  lgsquadlem2  27290  lgsquadlem3  27291  chebbnd1lem1  27378  dchrisum0re  27422  dchrisum0lema  27423  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem2  27427  tgisline  28572  elntg  28929  uhgrss  29009  upgrex  29037  edguhgr  29074  1loopgrvd0  29450  disjiunel  32540  suppovss  32624  elfzodif0  32738  nn0difffzod  32750  pfxchn  32952  chnind  32954  chnccats1  32958  gsumfs2d  33009  gsumhashmul  33015  odpmco  33029  pmtrcnel  33032  pmtrcnelor  33034  cycpmco2f1  33067  cycpmco2rn  33068  cycpmco2lem1  33069  cycpmco2lem2  33070  cycpmco2lem3  33071  cycpmco2lem4  33072  cycpmco2lem5  33073  cycpmco2lem6  33074  cycpmco2lem7  33075  cycpmco2  33076  cyc3co2  33083  tocyccntz  33087  cyc3conja  33100  fxpsdrg  33118  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrunlem2  33189  domnprodn0  33216  idomrcanOLD  33222  isdrng4  33235  fracfld  33248  lindssn  33316  lindfpropd  33320  elrspunidl  33366  elrspunsn  33367  drngidl  33371  mxidlmaxv  33406  mxidlirredi  33409  opprqusdrng  33431  qsdrnglem2  33434  rprmcl  33456  rprmirred  33469  pidufd  33481  1arithufdlem3  33484  dfufd2  33488  zringfrac  33492  ply1dg3rt0irred  33519  gsummoncoe1fzo  33531  lindsunlem  33597  fedgmullem1  33602  fedgmullem2  33603  assafld  33610  fldextrspunlsp  33647  extdgfialglem2  33666  irngnminplynz  33685  constrextdg2lem  33721  constrfiss  33724  constrsdrg  33748  submatminr1  33783  qtophaus  33809  qqhval2  33955  esummono  34027  gsumesum  34032  esum2dlem  34065  measvuni  34187  fiunelcarsg  34290  sitgclg  34316  sitgaddlemb  34322  eulerpartlemsv2  34332  eulerpartlemsv3  34335  eulerpartlemgc  34336  eulerpartlemv  34338  signstfvneq0  34546  signstfvcl  34547  signstfveq0a  34550  signstfveq0  34551  signsvfn  34556  signsvtp  34557  signsvtn  34558  signsvfpn  34559  signsvfnn  34560  signlem0  34561  hgt750leme  34632  onvf1odlem4  35089  iprodgam  35725  poimirlem2  37612  rrndstprj2  37821  lsatelbN  38995  lsatfixedN  38998  lkreqN  39159  lkrlspeqN  39160  dochnel2  41381  dochnel  41382  djhcvat42  41404  dochsnshp  41442  dochexmidat  41448  dochsnkr  41461  dochsnkr2  41462  dochsnkr2cl  41463  dochflcl  41464  dochfl1  41465  dochfln0  41466  lcfl6lem  41487  lcfl7lem  41488  lcfl8b  41493  lclkrlem2a  41496  lclkrlem2b  41497  lclkrlem2c  41498  lclkrlem2d  41499  lclkrlem2e  41500  lclkrlem2f  41501  lcfrlem14  41545  lcfrlem15  41546  lcfrlem16  41547  lcfrlem17  41548  lcfrlem18  41549  lcfrlem19  41550  lcfrlem20  41551  lcfrlem21  41552  lcfrlem23  41554  lcfrlem25  41556  lcfrlem26  41557  lcfrlem35  41566  lcfrlem36  41567  mapdn0  41658  mapdpglem29  41689  mapdpglem24  41693  baerlem3lem1  41696  baerlem5alem1  41697  baerlem5blem1  41698  baerlem3lem2  41699  baerlem5alem2  41700  baerlem5blem2  41701  baerlem5amN  41705  baerlem5bmN  41706  baerlem5abmN  41707  mapdindp0  41708  mapdindp1  41709  mapdindp2  41710  mapdindp3  41711  mapdindp4  41712  mapdheq2  41718  mapdheq4lem  41720  mapdheq4  41721  mapdh6lem1N  41722  mapdh6lem2N  41723  mapdh6aN  41724  mapdh6bN  41726  mapdh6cN  41727  mapdh6dN  41728  mapdh6eN  41729  mapdh6fN  41730  mapdh6gN  41731  mapdh6hN  41732  mapdh6iN  41733  mapdh7eN  41737  mapdh7cN  41738  mapdh7dN  41739  mapdh7fN  41740  mapdh75e  41741  mapdh75fN  41744  hvmaplfl  41756  mapdhvmap  41758  mapdh8aa  41765  mapdh8ab  41766  mapdh8ad  41768  mapdh8b  41769  mapdh8c  41770  mapdh8d0N  41771  mapdh8d  41772  mapdh8e  41773  mapdh9a  41778  mapdh9aOLDN  41779  hdmap1val2  41789  hdmap1eq  41790  hdmap1valc  41792  hdmap1eq2  41794  hdmap1eq4N  41795  hdmap1l6lem1  41796  hdmap1l6lem2  41797  hdmap1l6a  41798  hdmap1l6b  41800  hdmap1l6c  41801  hdmap1l6d  41802  hdmap1l6e  41803  hdmap1l6f  41804  hdmap1l6g  41805  hdmap1l6h  41806  hdmap1l6i  41807  hdmap1eulem  41811  hdmap1eulemOLDN  41812  hdmapcl  41819  hdmapval2lem  41820  hdmapval0  41822  hdmapeveclem  41823  hdmapevec  41824  hdmapval3lemN  41826  hdmapval3N  41827  hdmap10lem  41828  hdmap11lem1  41830  hdmap11lem2  41831  hdmapnzcl  41834  hdmaprnlem3N  41839  hdmaprnlem3uN  41840  hdmaprnlem4N  41842  hdmaprnlem7N  41844  hdmaprnlem8N  41845  hdmaprnlem9N  41846  hdmaprnlem3eN  41847  hdmaprnlem16N  41851  hdmap14lem1  41857  hdmap14lem2N  41858  hdmap14lem3  41859  hdmap14lem4a  41860  hdmap14lem6  41862  hdmap14lem8  41864  hdmap14lem9  41865  hdmap14lem10  41866  hdmap14lem11  41867  hdmap14lem12  41868  hgmaprnlem1N  41885  hgmaprnlem2N  41886  hgmaprnlem3N  41887  hgmaprnlem4N  41888  hdmapip1  41905  hdmapinvlem1  41907  hdmapinvlem2  41908  hdmapinvlem3  41909  hdmapinvlem4  41910  hdmapglem5  41911  hgmapvvlem1  41912  hgmapvvlem2  41913  hgmapvvlem3  41914  hdmapglem7a  41916  hdmapglem7b  41917  hdmapglem7  41918  evl1gprodd  42100  nelsubginvcld  42479  nelsubgcld  42480  nelsubgsubcld  42481  domnexpgn0cl  42506  fidomncyc  42518  prjspnfv01  42607  prjspner01  42608  prjspner1  42609  dffltz  42617  qirropth  42891  rmxyneg  42903  rmxm1  42917  rmxluc  42919  rmxdbl  42922  ltrmxnn0  42932  jm2.19lem1  42972  jm2.23  42979  rmxdiophlem  42998  aomclem2  43038  cantnftermord  43303  inaex  44280  bccm1k  44325  dstregt0  45274  fprodexp  45585  fprodabs2  45586  mccllem  45588  fprodcnlem  45590  climrec  45594  climdivf  45603  islpcn  45630  lptre2pt  45631  0ellimcdiv  45640  reclimc  45644  divlimc  45647  cncficcgt0  45879  dvdivf  45913  stoweidlem34  46025  stoweidlem43  46034  etransclem46  46271  etransclem47  46272  etransclem48  46273  hsphoidmvle2  46576  hsphoidmvle  46577  hoidmvlelem3  46588  hoidmvlelem4  46589  hspdifhsp  46607  readdcnnred  47297  resubcnnred  47298  recnmulnred  47299  cndivrenred  47300