Theorem eldifad 3974

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965

This theorem is referenced by:  xpdifid  6189  fvdifsupp  8194  unblem1  9325  cantnflem3  9728  cantnflem4  9729  oef1o  9735  infxpenc  10055  acndom2  10091  ackbij1lem18  10273  infpssrlem3  10342  fin23lem26  10362  fin23lem30  10379  pwfseqlem4a  10698  expclz  14121  symgextf  19449  pmtrfinv  19493  symggen  19502  efgsdmi  19764  efgs1b  19768  efgsp1  19769  efgsres  19770  efgredlemf  19773  efgredlemd  19776  efgredlemc  19777  efgredlem  19779  efgrelexlemb  19782  gsum2d2lem  20005  pgpfac1lem2  20109  pgpfac1lem3a  20110  pgpfac1lem3  20111  pgpfac1lem4  20112  zrzeroorngc  20660  zrtermoringc  20691  zrninitoringc  20692  domneq0r  20740  isdrng2  20759  fidomndrnglem  20789  lvecinv  21132  lspsncmp  21135  lspsnne1  21136  lspsnnecom  21138  lspabs2  21139  lspsneu  21142  lspdisjb  21145  lspexch  21148  lspindp1  21152  lvecindp2  21158  lspsolv  21162  lspsnat  21164  lsppratlem1  21166  lsppratlem2  21167  nzerooringczr  21508  frlmssuvc2  21832  evls1fpws  22388  maducoeval2  22661  hauscmplem  23429  1stccnp  23485  imasdsf1olem  24398  rrxmetlem  25454  divcncf  25495  dvrec  26007  dvmptdiv  26026  ftc1lem6  26096  elqaalem1  26375  elqaalem3  26377  ulmdvlem3  26459  abelthlem6  26494  abelthlem7a  26495  abelthlem7  26496  logtayl  26716  dmgmn0  27083  dmgmaddnn0  27084  dmgmdivn0  27085  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamgulm2  27093  lgambdd  27094  lgamucov  27095  lgamcvg2  27112  gamcvg  27113  gamcvg2lem  27116  ftalem3  27132  lgsqrlem1  27404  lgsqrlem2  27405  lgsqrlem3  27406  lgsqrlem4  27407  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgseisen  27437  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  chebbnd1lem1  27527  dchrisum0re  27571  dchrisum0lema  27572  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  tgisline  28649  elntg  29013  uhgrss  29095  upgrex  29123  edguhgr  29160  1loopgrvd0  29536  disjiunel  32615  suppovss  32695  nn0difffzod  32813  pfxchn  32983  chnind  32984  gsumfs2d  33040  gsumhashmul  33046  odpmco  33088  pmtrcnel  33091  pmtrcnelor  33093  cycpmco2f1  33126  cycpmco2rn  33127  cycpmco2lem1  33128  cycpmco2lem2  33129  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  cyc3co2  33142  tocyccntz  33146  cyc3conja  33159  elrgspnlem2  33232  elrgspnlem4  33234  domnprodn0  33261  idomrcanOLD  33265  isdrng4  33278  fracfld  33289  lindssn  33385  lindfpropd  33389  elrspunidl  33435  elrspunsn  33436  drngidl  33440  mxidlmaxv  33475  mxidlirredi  33478  opprqusdrng  33500  qsdrnglem2  33503  rprmcl  33525  rprmirred  33538  pidufd  33550  1arithufdlem3  33553  dfufd2  33557  zringfrac  33561  ply1dg3rt0irred  33586  gsummoncoe1fzo  33597  lindsunlem  33651  fedgmullem1  33656  fedgmullem2  33657  assafld  33664  irngnminplynz  33719  submatminr1  33770  qtophaus  33796  qqhval2  33944  esummono  34034  gsumesum  34039  esum2dlem  34072  measvuni  34194  fiunelcarsg  34297  sitgclg  34323  sitgaddlemb  34329  eulerpartlemsv2  34339  eulerpartlemsv3  34342  eulerpartlemgc  34343  eulerpartlemv  34345  signstfvneq0  34565  signstfvcl  34566  signstfveq0a  34569  signstfveq0  34570  signsvfn  34575  signsvtp  34576  signsvtn  34577  signsvfpn  34578  signsvfnn  34579  signlem0  34580  hgt750leme  34651  iprodgam  35721  poimirlem2  37608  rrndstprj2  37817  lsatelbN  38987  lsatfixedN  38990  lkreqN  39151  lkrlspeqN  39152  dochnel2  41374  dochnel  41375  djhcvat42  41397  dochsnshp  41435  dochexmidat  41441  dochsnkr  41454  dochsnkr2  41455  dochsnkr2cl  41456  dochflcl  41457  dochfl1  41458  dochfln0  41459  lcfl6lem  41480  lcfl7lem  41481  lcfl8b  41486  lclkrlem2a  41489  lclkrlem2b  41490  lclkrlem2c  41491  lclkrlem2d  41492  lclkrlem2e  41493  lclkrlem2f  41494  lcfrlem14  41538  lcfrlem15  41539  lcfrlem16  41540  lcfrlem17  41541  lcfrlem18  41542  lcfrlem19  41543  lcfrlem20  41544  lcfrlem21  41545  lcfrlem23  41547  lcfrlem25  41549  lcfrlem26  41550  lcfrlem35  41559  lcfrlem36  41560  mapdn0  41651  mapdpglem29  41682  mapdpglem24  41686  baerlem3lem1  41689  baerlem5alem1  41690  baerlem5blem1  41691  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  baerlem5amN  41698  baerlem5bmN  41699  baerlem5abmN  41700  mapdindp0  41701  mapdindp1  41702  mapdindp2  41703  mapdindp3  41704  mapdindp4  41705  mapdheq2  41711  mapdheq4lem  41713  mapdheq4  41714  mapdh6lem1N  41715  mapdh6lem2N  41716  mapdh6aN  41717  mapdh6bN  41719  mapdh6cN  41720  mapdh6dN  41721  mapdh6eN  41722  mapdh6fN  41723  mapdh6gN  41724  mapdh6hN  41725  mapdh6iN  41726  mapdh7eN  41730  mapdh7cN  41731  mapdh7dN  41732  mapdh7fN  41733  mapdh75e  41734  mapdh75fN  41737  hvmaplfl  41749  mapdhvmap  41751  mapdh8aa  41758  mapdh8ab  41759  mapdh8ad  41761  mapdh8b  41762  mapdh8c  41763  mapdh8d0N  41764  mapdh8d  41765  mapdh8e  41766  mapdh9a  41771  mapdh9aOLDN  41772  hdmap1val2  41782  hdmap1eq  41783  hdmap1valc  41785  hdmap1eq2  41787  hdmap1eq4N  41788  hdmap1l6lem1  41789  hdmap1l6lem2  41790  hdmap1l6a  41791  hdmap1l6b  41793  hdmap1l6c  41794  hdmap1l6d  41795  hdmap1l6e  41796  hdmap1l6f  41797  hdmap1l6g  41798  hdmap1l6h  41799  hdmap1l6i  41800  hdmap1eulem  41804  hdmap1eulemOLDN  41805  hdmapcl  41812  hdmapval2lem  41813  hdmapval0  41815  hdmapeveclem  41816  hdmapevec  41817  hdmapval3lemN  41819  hdmapval3N  41820  hdmap10lem  41821  hdmap11lem1  41823  hdmap11lem2  41824  hdmapnzcl  41827  hdmaprnlem3N  41832  hdmaprnlem3uN  41833  hdmaprnlem4N  41835  hdmaprnlem7N  41837  hdmaprnlem8N  41838  hdmaprnlem9N  41839  hdmaprnlem3eN  41840  hdmaprnlem16N  41844  hdmap14lem1  41850  hdmap14lem2N  41851  hdmap14lem3  41852  hdmap14lem4a  41853  hdmap14lem6  41855  hdmap14lem8  41857  hdmap14lem9  41858  hdmap14lem10  41859  hdmap14lem11  41860  hdmap14lem12  41861  hgmaprnlem1N  41878  hgmaprnlem2N  41879  hgmaprnlem3N  41880  hgmaprnlem4N  41881  hdmapip1  41898  hdmapinvlem1  41900  hdmapinvlem2  41901  hdmapinvlem3  41902  hdmapinvlem4  41903  hdmapglem5  41904  hgmapvvlem1  41905  hgmapvvlem2  41906  hgmapvvlem3  41907  hdmapglem7a  41909  hdmapglem7b  41910  hdmapglem7  41911  evl1gprodd  42098  nelsubginvcld  42482  nelsubgcld  42483  nelsubgsubcld  42484  domnexpgn0cl  42509  fidomncyc  42521  prjspnfv01  42610  prjspner01  42611  prjspner1  42612  dffltz  42620  qirropth  42895  rmxyneg  42908  rmxm1  42922  rmxluc  42924  rmxdbl  42927  ltrmxnn0  42937  jm2.19lem1  42977  jm2.23  42984  rmxdiophlem  43003  aomclem2  43043  cantnftermord  43309  inaex  44292  bccm1k  44337  dstregt0  45231  fprodexp  45549  fprodabs2  45550  mccllem  45552  fprodcnlem  45554  climrec  45558  climdivf  45567  islpcn  45594  lptre2pt  45595  0ellimcdiv  45604  reclimc  45608  divlimc  45611  cncficcgt0  45843  dvdivf  45877  stoweidlem34  45989  stoweidlem43  45998  etransclem46  46235  etransclem47  46236  etransclem48  46237  hsphoidmvle2  46540  hsphoidmvle  46541  hoidmvlelem3  46552  hoidmvlelem4  46553  hspdifhsp  46571  readdcnnred  47252  resubcnnred  47253  recnmulnred  47254  cndivrenred  47255