Theorem eldifad 3938

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929

This theorem is referenced by:  xpdifid  6157  fvdifsupp  8168  unblem1  9298  cantnflem3  9703  cantnflem4  9704  oef1o  9710  infxpenc  10030  acndom2  10066  ackbij1lem18  10248  infpssrlem3  10317  fin23lem26  10337  fin23lem30  10354  pwfseqlem4a  10673  expclz  14100  symgextf  19396  pmtrfinv  19440  symggen  19449  efgsdmi  19711  efgs1b  19715  efgsp1  19716  efgsres  19717  efgredlemf  19720  efgredlemd  19723  efgredlemc  19724  efgredlem  19726  efgrelexlemb  19729  gsum2d2lem  19952  pgpfac1lem2  20056  pgpfac1lem3a  20057  pgpfac1lem3  20058  pgpfac1lem4  20059  zrzeroorngc  20602  zrtermoringc  20633  zrninitoringc  20634  domneq0r  20682  isdrng2  20701  fidomndrnglem  20730  lvecinv  21072  lspsncmp  21075  lspsnne1  21076  lspsnnecom  21078  lspabs2  21079  lspsneu  21082  lspdisjb  21085  lspexch  21088  lspindp1  21092  lvecindp2  21098  lspsolv  21102  lspsnat  21104  lsppratlem1  21106  lsppratlem2  21107  nzerooringczr  21439  frlmssuvc2  21753  evls1fpws  22305  maducoeval2  22576  hauscmplem  23342  1stccnp  23398  imasdsf1olem  24310  rrxmetlem  25357  divcncf  25398  dvrec  25909  dvmptdiv  25928  ftc1lem6  25998  elqaalem1  26277  elqaalem3  26279  ulmdvlem3  26361  abelthlem6  26396  abelthlem7a  26397  abelthlem7  26398  logtayl  26619  dmgmn0  26986  dmgmaddnn0  26987  dmgmdivn0  26988  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem5  26993  lgamgulmlem6  26994  lgamgulm2  26996  lgambdd  26997  lgamucov  26998  lgamcvg2  27015  gamcvg  27016  gamcvg2lem  27019  ftalem3  27035  lgsqrlem1  27307  lgsqrlem2  27308  lgsqrlem3  27309  lgsqrlem4  27310  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgseisenlem4  27339  lgseisen  27340  lgsquadlem1  27341  lgsquadlem2  27342  lgsquadlem3  27343  chebbnd1lem1  27430  dchrisum0re  27474  dchrisum0lema  27475  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  tgisline  28552  elntg  28909  uhgrss  28989  upgrex  29017  edguhgr  29054  1loopgrvd0  29430  disjiunel  32523  suppovss  32604  elfzodif0  32717  nn0difffzod  32729  pfxchn  32935  chnind  32937  chnccats1  32941  gsumfs2d  32995  gsumhashmul  33001  odpmco  33043  pmtrcnel  33046  pmtrcnelor  33048  cycpmco2f1  33081  cycpmco2rn  33082  cycpmco2lem1  33083  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  cyc3co2  33097  tocyccntz  33101  cyc3conja  33114  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrunlem2  33189  domnprodn0  33216  idomrcanOLD  33222  isdrng4  33235  fracfld  33248  lindssn  33339  lindfpropd  33343  elrspunidl  33389  elrspunsn  33390  drngidl  33394  mxidlmaxv  33429  mxidlirredi  33432  opprqusdrng  33454  qsdrnglem2  33457  rprmcl  33479  rprmirred  33492  pidufd  33504  1arithufdlem3  33507  dfufd2  33511  zringfrac  33515  ply1dg3rt0irred  33541  gsummoncoe1fzo  33553  lindsunlem  33610  fedgmullem1  33615  fedgmullem2  33616  assafld  33623  fldextrspunlsp  33661  irngnminplynz  33692  constrextdg2lem  33728  constrfiss  33731  constrsdrg  33755  submatminr1  33787  qtophaus  33813  qqhval2  33959  esummono  34031  gsumesum  34036  esum2dlem  34069  measvuni  34191  fiunelcarsg  34294  sitgclg  34320  sitgaddlemb  34326  eulerpartlemsv2  34336  eulerpartlemsv3  34339  eulerpartlemgc  34340  eulerpartlemv  34342  signstfvneq0  34550  signstfvcl  34551  signstfveq0a  34554  signstfveq0  34555  signsvfn  34560  signsvtp  34561  signsvtn  34562  signsvfpn  34563  signsvfnn  34564  signlem0  34565  hgt750leme  34636  iprodgam  35705  poimirlem2  37592  rrndstprj2  37801  lsatelbN  38970  lsatfixedN  38973  lkreqN  39134  lkrlspeqN  39135  dochnel2  41357  dochnel  41358  djhcvat42  41380  dochsnshp  41418  dochexmidat  41424  dochsnkr  41437  dochsnkr2  41438  dochsnkr2cl  41439  dochflcl  41440  dochfl1  41441  dochfln0  41442  lcfl6lem  41463  lcfl7lem  41464  lcfl8b  41469  lclkrlem2a  41472  lclkrlem2b  41473  lclkrlem2c  41474  lclkrlem2d  41475  lclkrlem2e  41476  lclkrlem2f  41477  lcfrlem14  41521  lcfrlem15  41522  lcfrlem16  41523  lcfrlem17  41524  lcfrlem18  41525  lcfrlem19  41526  lcfrlem20  41527  lcfrlem21  41528  lcfrlem23  41530  lcfrlem25  41532  lcfrlem26  41533  lcfrlem35  41542  lcfrlem36  41543  mapdn0  41634  mapdpglem29  41665  mapdpglem24  41669  baerlem3lem1  41672  baerlem5alem1  41673  baerlem5blem1  41674  baerlem3lem2  41675  baerlem5alem2  41676  baerlem5blem2  41677  baerlem5amN  41681  baerlem5bmN  41682  baerlem5abmN  41683  mapdindp0  41684  mapdindp1  41685  mapdindp2  41686  mapdindp3  41687  mapdindp4  41688  mapdheq2  41694  mapdheq4lem  41696  mapdheq4  41697  mapdh6lem1N  41698  mapdh6lem2N  41699  mapdh6aN  41700  mapdh6bN  41702  mapdh6cN  41703  mapdh6dN  41704  mapdh6eN  41705  mapdh6fN  41706  mapdh6gN  41707  mapdh6hN  41708  mapdh6iN  41709  mapdh7eN  41713  mapdh7cN  41714  mapdh7dN  41715  mapdh7fN  41716  mapdh75e  41717  mapdh75fN  41720  hvmaplfl  41732  mapdhvmap  41734  mapdh8aa  41741  mapdh8ab  41742  mapdh8ad  41744  mapdh8b  41745  mapdh8c  41746  mapdh8d0N  41747  mapdh8d  41748  mapdh8e  41749  mapdh9a  41754  mapdh9aOLDN  41755  hdmap1val2  41765  hdmap1eq  41766  hdmap1valc  41768  hdmap1eq2  41770  hdmap1eq4N  41771  hdmap1l6lem1  41772  hdmap1l6lem2  41773  hdmap1l6a  41774  hdmap1l6b  41776  hdmap1l6c  41777  hdmap1l6d  41778  hdmap1l6e  41779  hdmap1l6f  41780  hdmap1l6g  41781  hdmap1l6h  41782  hdmap1l6i  41783  hdmap1eulem  41787  hdmap1eulemOLDN  41788  hdmapcl  41795  hdmapval2lem  41796  hdmapval0  41798  hdmapeveclem  41799  hdmapevec  41800  hdmapval3lemN  41802  hdmapval3N  41803  hdmap10lem  41804  hdmap11lem1  41806  hdmap11lem2  41807  hdmapnzcl  41810  hdmaprnlem3N  41815  hdmaprnlem3uN  41816  hdmaprnlem4N  41818  hdmaprnlem7N  41820  hdmaprnlem8N  41821  hdmaprnlem9N  41822  hdmaprnlem3eN  41823  hdmaprnlem16N  41827  hdmap14lem1  41833  hdmap14lem2N  41834  hdmap14lem3  41835  hdmap14lem4a  41836  hdmap14lem6  41838  hdmap14lem8  41840  hdmap14lem9  41841  hdmap14lem10  41842  hdmap14lem11  41843  hdmap14lem12  41844  hgmaprnlem1N  41861  hgmaprnlem2N  41862  hgmaprnlem3N  41863  hgmaprnlem4N  41864  hdmapip1  41881  hdmapinvlem1  41883  hdmapinvlem2  41884  hdmapinvlem3  41885  hdmapinvlem4  41886  hdmapglem5  41887  hgmapvvlem1  41888  hgmapvvlem2  41889  hgmapvvlem3  41890  hdmapglem7a  41892  hdmapglem7b  41893  hdmapglem7  41894  evl1gprodd  42076  nelsubginvcld  42466  nelsubgcld  42467  nelsubgsubcld  42468  domnexpgn0cl  42493  fidomncyc  42505  prjspnfv01  42594  prjspner01  42595  prjspner1  42596  dffltz  42604  qirropth  42878  rmxyneg  42891  rmxm1  42905  rmxluc  42907  rmxdbl  42910  ltrmxnn0  42920  jm2.19lem1  42960  jm2.23  42967  rmxdiophlem  42986  aomclem2  43026  cantnftermord  43291  inaex  44269  bccm1k  44314  dstregt0  45258  fprodexp  45571  fprodabs2  45572  mccllem  45574  fprodcnlem  45576  climrec  45580  climdivf  45589  islpcn  45616  lptre2pt  45617  0ellimcdiv  45626  reclimc  45630  divlimc  45633  cncficcgt0  45865  dvdivf  45899  stoweidlem34  46011  stoweidlem43  46020  etransclem46  46257  etransclem47  46258  etransclem48  46259  hsphoidmvle2  46562  hsphoidmvle  46563  hoidmvlelem3  46574  hoidmvlelem4  46575  hspdifhsp  46593  readdcnnred  47280  resubcnnred  47281  recnmulnred  47282  cndivrenred  47283