Theorem eldifad 3902

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893

This theorem is referenced by:  xpdifid  6127  fvdifsupp  8115  unblem1  9196  cantnflem3  9606  cantnflem4  9607  oef1o  9613  infxpenc  9934  acndom2  9970  ackbij1lem18  10152  infpssrlem3  10221  fin23lem26  10241  fin23lem30  10258  pwfseqlem4a  10578  elfzodif0  13719  expclz  14040  pfxchn  18570  chnind  18581  chnccats1  18585  chnccat  18586  symgextf  19386  pmtrfinv  19430  symggen  19439  efgsdmi  19701  efgs1b  19705  efgsp1  19706  efgsres  19707  efgredlemf  19710  efgredlemd  19713  efgredlemc  19714  efgredlem  19716  efgrelexlemb  19719  gsum2d2lem  19942  pgpfac1lem2  20046  pgpfac1lem3a  20047  pgpfac1lem3  20048  pgpfac1lem4  20049  zrzeroorngc  20615  zrtermoringc  20646  zrninitoringc  20647  domneq0r  20695  isdrng2  20714  fidomndrnglem  20743  lvecinv  21106  lspsncmp  21109  lspsnne1  21110  lspsnnecom  21112  lspabs2  21113  lspsneu  21116  lspdisjb  21119  lspexch  21122  lspindp1  21126  lvecindp2  21132  lspsolv  21136  lspsnat  21138  lsppratlem1  21140  lsppratlem2  21141  nzerooringczr  21473  frlmssuvc2  21788  evls1fpws  22347  maducoeval2  22618  hauscmplem  23384  1stccnp  23440  imasdsf1olem  24351  rrxmetlem  25387  divcncf  25427  dvrec  25935  dvmptdiv  25954  ftc1lem6  26021  elqaalem1  26299  elqaalem3  26301  ulmdvlem3  26383  abelthlem6  26417  abelthlem7a  26418  abelthlem7  26419  logtayl  26640  dmgmn0  27006  dmgmaddnn0  27007  dmgmdivn0  27008  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamgulmlem5  27013  lgamgulmlem6  27014  lgamgulm2  27016  lgambdd  27017  lgamucov  27018  lgamcvg2  27035  gamcvg  27036  gamcvg2lem  27039  ftalem3  27055  lgsqrlem1  27326  lgsqrlem2  27327  lgsqrlem3  27328  lgsqrlem4  27329  lgseisenlem1  27355  lgseisenlem2  27356  lgseisenlem3  27357  lgseisenlem4  27358  lgseisen  27359  lgsquadlem1  27360  lgsquadlem2  27361  lgsquadlem3  27362  chebbnd1lem1  27449  dchrisum0re  27493  dchrisum0lema  27494  dchrisum0lem1b  27495  dchrisum0lem1  27496  dchrisum0lem2a  27497  dchrisum0lem2  27498  tgisline  28712  elntg  29070  uhgrss  29150  upgrex  29178  edguhgr  29215  1loopgrvd0  29591  disjiunel  32684  suppovss  32772  nn0difffzod  32895  gsumfs2d  33140  gsumhashmul  33146  suppgsumssiun  33151  odpmco  33165  pmtrcnel  33168  pmtrcnelor  33170  cycpmco2f1  33203  cycpmco2rn  33204  cycpmco2lem1  33205  cycpmco2lem2  33206  cycpmco2lem3  33207  cycpmco2lem4  33208  cycpmco2lem5  33209  cycpmco2lem6  33210  cycpmco2lem7  33211  cycpmco2  33212  cyc3co2  33219  tocyccntz  33223  cyc3conja  33236  fxpsdrg  33254  elrgspnlem2  33322  elrgspnlem4  33324  elrgspnsubrunlem2  33327  domnprodn0  33354  domnprodeq0  33355  idomrcanOLD  33361  isdrng4  33374  fracfld  33387  lindssn  33456  lindfpropd  33460  elrspunidl  33506  elrspunsn  33507  drngidl  33511  mxidlmaxv  33546  mxidlirredi  33549  opprqusdrng  33571  qsdrnglem2  33574  rprmcl  33596  rprmirred  33609  pidufd  33621  1arithufdlem3  33624  dfufd2  33628  zringfrac  33632  deg1prod  33661  ply1dg3rt0irred  33662  gsummoncoe1fzo  33675  mplvrpmrhm  33709  psrgsum  33710  psrmonprod  33714  esplyfval2  33727  lindsunlem  33787  fedgmullem1  33792  fedgmullem2  33793  assafld  33800  fldextrspunlsp  33837  extdgfialglem2  33856  irngnminplynz  33875  constrextdg2lem  33911  constrfiss  33914  constrsdrg  33938  submatminr1  33973  qtophaus  33999  qqhval2  34145  esummono  34217  gsumesum  34222  esum2dlem  34255  measvuni  34377  fiunelcarsg  34479  sitgclg  34505  sitgaddlemb  34511  eulerpartlemsv2  34521  eulerpartlemsv3  34524  eulerpartlemgc  34525  eulerpartlemv  34527  signstfvneq0  34735  signstfvcl  34736  signstfveq0a  34739  signstfveq0  34740  signsvfn  34745  signsvtp  34746  signsvtn  34747  signsvfpn  34748  signsvfnn  34749  signlem0  34750  hgt750leme  34821  onvf1odlem4  35307  iprodgam  35943  ttcwf2  36726  mh-inf3f1  36742  poimirlem2  37960  rrndstprj2  38169  lsatelbN  39469  lsatfixedN  39472  lkreqN  39633  lkrlspeqN  39634  dochnel2  41855  dochnel  41856  djhcvat42  41878  dochsnshp  41916  dochexmidat  41922  dochsnkr  41935  dochsnkr2  41936  dochsnkr2cl  41937  dochflcl  41938  dochfl1  41939  dochfln0  41940  lcfl6lem  41961  lcfl7lem  41962  lcfl8b  41967  lclkrlem2a  41970  lclkrlem2b  41971  lclkrlem2c  41972  lclkrlem2d  41973  lclkrlem2e  41974  lclkrlem2f  41975  lcfrlem14  42019  lcfrlem15  42020  lcfrlem16  42021  lcfrlem17  42022  lcfrlem18  42023  lcfrlem19  42024  lcfrlem20  42025  lcfrlem21  42026  lcfrlem23  42028  lcfrlem25  42030  lcfrlem26  42031  lcfrlem35  42040  lcfrlem36  42041  mapdn0  42132  mapdpglem29  42163  mapdpglem24  42167  baerlem3lem1  42170  baerlem5alem1  42171  baerlem5blem1  42172  baerlem3lem2  42173  baerlem5alem2  42174  baerlem5blem2  42175  baerlem5amN  42179  baerlem5bmN  42180  baerlem5abmN  42181  mapdindp0  42182  mapdindp1  42183  mapdindp2  42184  mapdindp3  42185  mapdindp4  42186  mapdheq2  42192  mapdheq4lem  42194  mapdheq4  42195  mapdh6lem1N  42196  mapdh6lem2N  42197  mapdh6aN  42198  mapdh6bN  42200  mapdh6cN  42201  mapdh6dN  42202  mapdh6eN  42203  mapdh6fN  42204  mapdh6gN  42205  mapdh6hN  42206  mapdh6iN  42207  mapdh7eN  42211  mapdh7cN  42212  mapdh7dN  42213  mapdh7fN  42214  mapdh75e  42215  mapdh75fN  42218  hvmaplfl  42230  mapdhvmap  42232  mapdh8aa  42239  mapdh8ab  42240  mapdh8ad  42242  mapdh8b  42243  mapdh8c  42244  mapdh8d0N  42245  mapdh8d  42246  mapdh8e  42247  mapdh9a  42252  mapdh9aOLDN  42253  hdmap1val2  42263  hdmap1eq  42264  hdmap1valc  42266  hdmap1eq2  42268  hdmap1eq4N  42269  hdmap1l6lem1  42270  hdmap1l6lem2  42271  hdmap1l6a  42272  hdmap1l6b  42274  hdmap1l6c  42275  hdmap1l6d  42276  hdmap1l6e  42277  hdmap1l6f  42278  hdmap1l6g  42279  hdmap1l6h  42280  hdmap1l6i  42281  hdmap1eulem  42285  hdmap1eulemOLDN  42286  hdmapcl  42293  hdmapval2lem  42294  hdmapval0  42296  hdmapeveclem  42297  hdmapevec  42298  hdmapval3lemN  42300  hdmapval3N  42301  hdmap10lem  42302  hdmap11lem1  42304  hdmap11lem2  42305  hdmapnzcl  42308  hdmaprnlem3N  42313  hdmaprnlem3uN  42314  hdmaprnlem4N  42316  hdmaprnlem7N  42318  hdmaprnlem8N  42319  hdmaprnlem9N  42320  hdmaprnlem3eN  42321  hdmaprnlem16N  42325  hdmap14lem1  42331  hdmap14lem2N  42332  hdmap14lem3  42333  hdmap14lem4a  42334  hdmap14lem6  42336  hdmap14lem8  42338  hdmap14lem9  42339  hdmap14lem10  42340  hdmap14lem11  42341  hdmap14lem12  42342  hgmaprnlem1N  42359  hgmaprnlem2N  42360  hgmaprnlem3N  42361  hgmaprnlem4N  42362  hdmapip1  42379  hdmapinvlem1  42381  hdmapinvlem2  42382  hdmapinvlem3  42383  hdmapinvlem4  42384  hdmapglem5  42385  hgmapvvlem1  42386  hgmapvvlem2  42387  hgmapvvlem3  42388  hdmapglem7a  42390  hdmapglem7b  42391  hdmapglem7  42392  evl1gprodd  42573  nelsubginvcld  42958  nelsubgcld  42959  nelsubgsubcld  42960  domnexpgn0cl  42985  fidomncyc  42997  prjspnfv01  43074  prjspner01  43075  prjspner1  43076  dffltz  43084  qirropth  43357  rmxyneg  43369  rmxm1  43383  rmxluc  43385  rmxdbl  43388  ltrmxnn0  43398  jm2.19lem1  43438  jm2.23  43445  rmxdiophlem  43464  aomclem2  43504  cantnftermord  43769  inaex  44745  bccm1k  44790  dstregt0  45736  fprodexp  46045  fprodabs2  46046  mccllem  46048  fprodcnlem  46050  climrec  46054  climdivf  46063  islpcn  46088  lptre2pt  46089  0ellimcdiv  46098  reclimc  46102  divlimc  46105  cncficcgt0  46337  dvdivf  46371  stoweidlem34  46483  stoweidlem43  46492  etransclem46  46729  etransclem47  46730  etransclem48  46731  hsphoidmvle2  47034  hsphoidmvle  47035  hoidmvlelem3  47046  hoidmvlelem4  47047  hspdifhsp  47065  readdcnnred  47766  resubcnnred  47767  recnmulnred  47768  cndivrenred  47769