Theorem eldifad 3909

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900

This theorem is referenced by:  xpdifid  6115  fvdifsupp  8101  unblem1  9176  cantnflem3  9581  cantnflem4  9582  oef1o  9588  infxpenc  9909  acndom2  9945  ackbij1lem18  10127  infpssrlem3  10196  fin23lem26  10216  fin23lem30  10233  pwfseqlem4a  10552  elfzodif0  13670  expclz  13991  pfxchn  18516  chnind  18527  chnccats1  18531  chnccat  18532  symgextf  19329  pmtrfinv  19373  symggen  19382  efgsdmi  19644  efgs1b  19648  efgsp1  19649  efgsres  19650  efgredlemf  19653  efgredlemd  19656  efgredlemc  19657  efgredlem  19659  efgrelexlemb  19662  gsum2d2lem  19885  pgpfac1lem2  19989  pgpfac1lem3a  19990  pgpfac1lem3  19991  pgpfac1lem4  19992  zrzeroorngc  20559  zrtermoringc  20590  zrninitoringc  20591  domneq0r  20639  isdrng2  20658  fidomndrnglem  20687  lvecinv  21050  lspsncmp  21053  lspsnne1  21054  lspsnnecom  21056  lspabs2  21057  lspsneu  21060  lspdisjb  21063  lspexch  21066  lspindp1  21070  lvecindp2  21076  lspsolv  21080  lspsnat  21082  lsppratlem1  21084  lsppratlem2  21085  nzerooringczr  21417  frlmssuvc2  21732  evls1fpws  22284  maducoeval2  22555  hauscmplem  23321  1stccnp  23377  imasdsf1olem  24288  rrxmetlem  25334  divcncf  25375  dvrec  25886  dvmptdiv  25905  ftc1lem6  25975  elqaalem1  26254  elqaalem3  26256  ulmdvlem3  26338  abelthlem6  26373  abelthlem7a  26374  abelthlem7  26375  logtayl  26596  dmgmn0  26963  dmgmaddnn0  26964  dmgmdivn0  26965  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamgulmlem5  26970  lgamgulmlem6  26971  lgamgulm2  26973  lgambdd  26974  lgamucov  26975  lgamcvg2  26992  gamcvg  26993  gamcvg2lem  26996  ftalem3  27012  lgsqrlem1  27284  lgsqrlem2  27285  lgsqrlem3  27286  lgsqrlem4  27287  lgseisenlem1  27313  lgseisenlem2  27314  lgseisenlem3  27315  lgseisenlem4  27316  lgseisen  27317  lgsquadlem1  27318  lgsquadlem2  27319  lgsquadlem3  27320  chebbnd1lem1  27407  dchrisum0re  27451  dchrisum0lema  27452  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2a  27455  dchrisum0lem2  27456  tgisline  28605  elntg  28962  uhgrss  29042  upgrex  29070  edguhgr  29107  1loopgrvd0  29483  disjiunel  32576  suppovss  32662  nn0difffzod  32786  gsumfs2d  33035  gsumhashmul  33041  odpmco  33055  pmtrcnel  33058  pmtrcnelor  33060  cycpmco2f1  33093  cycpmco2rn  33094  cycpmco2lem1  33095  cycpmco2lem2  33096  cycpmco2lem3  33097  cycpmco2lem4  33098  cycpmco2lem5  33099  cycpmco2lem6  33100  cycpmco2lem7  33101  cycpmco2  33102  cyc3co2  33109  tocyccntz  33113  cyc3conja  33126  fxpsdrg  33144  elrgspnlem2  33210  elrgspnlem4  33212  elrgspnsubrunlem2  33215  domnprodn0  33242  idomrcanOLD  33248  isdrng4  33261  fracfld  33274  lindssn  33343  lindfpropd  33347  elrspunidl  33393  elrspunsn  33394  drngidl  33398  mxidlmaxv  33433  mxidlirredi  33436  opprqusdrng  33458  qsdrnglem2  33461  rprmcl  33483  rprmirred  33496  pidufd  33508  1arithufdlem3  33511  dfufd2  33515  zringfrac  33519  ply1dg3rt0irred  33546  gsummoncoe1fzo  33558  mplvrpmrhm  33577  lindsunlem  33637  fedgmullem1  33642  fedgmullem2  33643  assafld  33650  fldextrspunlsp  33687  extdgfialglem2  33706  irngnminplynz  33725  constrextdg2lem  33761  constrfiss  33764  constrsdrg  33788  submatminr1  33823  qtophaus  33849  qqhval2  33995  esummono  34067  gsumesum  34072  esum2dlem  34105  measvuni  34227  fiunelcarsg  34329  sitgclg  34355  sitgaddlemb  34361  eulerpartlemsv2  34371  eulerpartlemsv3  34374  eulerpartlemgc  34375  eulerpartlemv  34377  signstfvneq0  34585  signstfvcl  34586  signstfveq0a  34589  signstfveq0  34590  signsvfn  34595  signsvtp  34596  signsvtn  34597  signsvfpn  34598  signsvfnn  34599  signlem0  34600  hgt750leme  34671  onvf1odlem4  35150  iprodgam  35786  poimirlem2  37672  rrndstprj2  37881  lsatelbN  39115  lsatfixedN  39118  lkreqN  39279  lkrlspeqN  39280  dochnel2  41501  dochnel  41502  djhcvat42  41524  dochsnshp  41562  dochexmidat  41568  dochsnkr  41581  dochsnkr2  41582  dochsnkr2cl  41583  dochflcl  41584  dochfl1  41585  dochfln0  41586  lcfl6lem  41607  lcfl7lem  41608  lcfl8b  41613  lclkrlem2a  41616  lclkrlem2b  41617  lclkrlem2c  41618  lclkrlem2d  41619  lclkrlem2e  41620  lclkrlem2f  41621  lcfrlem14  41665  lcfrlem15  41666  lcfrlem16  41667  lcfrlem17  41668  lcfrlem18  41669  lcfrlem19  41670  lcfrlem20  41671  lcfrlem21  41672  lcfrlem23  41674  lcfrlem25  41676  lcfrlem26  41677  lcfrlem35  41686  lcfrlem36  41687  mapdn0  41778  mapdpglem29  41809  mapdpglem24  41813  baerlem3lem1  41816  baerlem5alem1  41817  baerlem5blem1  41818  baerlem3lem2  41819  baerlem5alem2  41820  baerlem5blem2  41821  baerlem5amN  41825  baerlem5bmN  41826  baerlem5abmN  41827  mapdindp0  41828  mapdindp1  41829  mapdindp2  41830  mapdindp3  41831  mapdindp4  41832  mapdheq2  41838  mapdheq4lem  41840  mapdheq4  41841  mapdh6lem1N  41842  mapdh6lem2N  41843  mapdh6aN  41844  mapdh6bN  41846  mapdh6cN  41847  mapdh6dN  41848  mapdh6eN  41849  mapdh6fN  41850  mapdh6gN  41851  mapdh6hN  41852  mapdh6iN  41853  mapdh7eN  41857  mapdh7cN  41858  mapdh7dN  41859  mapdh7fN  41860  mapdh75e  41861  mapdh75fN  41864  hvmaplfl  41876  mapdhvmap  41878  mapdh8aa  41885  mapdh8ab  41886  mapdh8ad  41888  mapdh8b  41889  mapdh8c  41890  mapdh8d0N  41891  mapdh8d  41892  mapdh8e  41893  mapdh9a  41898  mapdh9aOLDN  41899  hdmap1val2  41909  hdmap1eq  41910  hdmap1valc  41912  hdmap1eq2  41914  hdmap1eq4N  41915  hdmap1l6lem1  41916  hdmap1l6lem2  41917  hdmap1l6a  41918  hdmap1l6b  41920  hdmap1l6c  41921  hdmap1l6d  41922  hdmap1l6e  41923  hdmap1l6f  41924  hdmap1l6g  41925  hdmap1l6h  41926  hdmap1l6i  41927  hdmap1eulem  41931  hdmap1eulemOLDN  41932  hdmapcl  41939  hdmapval2lem  41940  hdmapval0  41942  hdmapeveclem  41943  hdmapevec  41944  hdmapval3lemN  41946  hdmapval3N  41947  hdmap10lem  41948  hdmap11lem1  41950  hdmap11lem2  41951  hdmapnzcl  41954  hdmaprnlem3N  41959  hdmaprnlem3uN  41960  hdmaprnlem4N  41962  hdmaprnlem7N  41964  hdmaprnlem8N  41965  hdmaprnlem9N  41966  hdmaprnlem3eN  41967  hdmaprnlem16N  41971  hdmap14lem1  41977  hdmap14lem2N  41978  hdmap14lem3  41979  hdmap14lem4a  41980  hdmap14lem6  41982  hdmap14lem8  41984  hdmap14lem9  41985  hdmap14lem10  41986  hdmap14lem11  41987  hdmap14lem12  41988  hgmaprnlem1N  42005  hgmaprnlem2N  42006  hgmaprnlem3N  42007  hgmaprnlem4N  42008  hdmapip1  42025  hdmapinvlem1  42027  hdmapinvlem2  42028  hdmapinvlem3  42029  hdmapinvlem4  42030  hdmapglem5  42031  hgmapvvlem1  42032  hgmapvvlem2  42033  hgmapvvlem3  42034  hdmapglem7a  42036  hdmapglem7b  42037  hdmapglem7  42038  evl1gprodd  42220  nelsubginvcld  42599  nelsubgcld  42600  nelsubgsubcld  42601  domnexpgn0cl  42626  fidomncyc  42638  prjspnfv01  42727  prjspner01  42728  prjspner1  42729  dffltz  42737  qirropth  43011  rmxyneg  43023  rmxm1  43037  rmxluc  43039  rmxdbl  43042  ltrmxnn0  43052  jm2.19lem1  43092  jm2.23  43099  rmxdiophlem  43118  aomclem2  43158  cantnftermord  43423  inaex  44400  bccm1k  44445  dstregt0  45393  fprodexp  45704  fprodabs2  45705  mccllem  45707  fprodcnlem  45709  climrec  45713  climdivf  45722  islpcn  45747  lptre2pt  45748  0ellimcdiv  45757  reclimc  45761  divlimc  45764  cncficcgt0  45996  dvdivf  46030  stoweidlem34  46142  stoweidlem43  46151  etransclem46  46388  etransclem47  46389  etransclem48  46390  hsphoidmvle2  46693  hsphoidmvle  46694  hoidmvlelem3  46705  hoidmvlelem4  46706  hspdifhsp  46724  readdcnnred  47413  resubcnnred  47414  recnmulnred  47415  cndivrenred  47416