Theorem eldifad 3926

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

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

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 3449  df-dif 3917

This theorem is referenced by:  xpdifid  6141  fvdifsupp  8150  unblem1  9239  cantnflem3  9644  cantnflem4  9645  oef1o  9651  infxpenc  9971  acndom2  10007  ackbij1lem18  10189  infpssrlem3  10258  fin23lem26  10278  fin23lem30  10295  pwfseqlem4a  10614  expclz  14049  symgextf  19347  pmtrfinv  19391  symggen  19400  efgsdmi  19662  efgs1b  19666  efgsp1  19667  efgsres  19668  efgredlemf  19671  efgredlemd  19674  efgredlemc  19675  efgredlem  19677  efgrelexlemb  19680  gsum2d2lem  19903  pgpfac1lem2  20007  pgpfac1lem3a  20008  pgpfac1lem3  20009  pgpfac1lem4  20010  zrzeroorngc  20553  zrtermoringc  20584  zrninitoringc  20585  domneq0r  20633  isdrng2  20652  fidomndrnglem  20681  lvecinv  21023  lspsncmp  21026  lspsnne1  21027  lspsnnecom  21029  lspabs2  21030  lspsneu  21033  lspdisjb  21036  lspexch  21039  lspindp1  21043  lvecindp2  21049  lspsolv  21053  lspsnat  21055  lsppratlem1  21057  lsppratlem2  21058  nzerooringczr  21390  frlmssuvc2  21704  evls1fpws  22256  maducoeval2  22527  hauscmplem  23293  1stccnp  23349  imasdsf1olem  24261  rrxmetlem  25307  divcncf  25348  dvrec  25859  dvmptdiv  25878  ftc1lem6  25948  elqaalem1  26227  elqaalem3  26229  ulmdvlem3  26311  abelthlem6  26346  abelthlem7a  26347  abelthlem7  26348  logtayl  26569  dmgmn0  26936  dmgmaddnn0  26937  dmgmdivn0  26938  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamgulm2  26946  lgambdd  26947  lgamucov  26948  lgamcvg2  26965  gamcvg  26966  gamcvg2lem  26969  ftalem3  26985  lgsqrlem1  27257  lgsqrlem2  27258  lgsqrlem3  27259  lgsqrlem4  27260  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgseisen  27290  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  chebbnd1lem1  27380  dchrisum0re  27424  dchrisum0lema  27425  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  tgisline  28554  elntg  28911  uhgrss  28991  upgrex  29019  edguhgr  29056  1loopgrvd0  29432  disjiunel  32525  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  33194  elrgspnlem4  33196  elrgspnsubrunlem2  33199  domnprodn0  33226  idomrcanOLD  33232  isdrng4  33245  fracfld  33258  lindssn  33349  lindfpropd  33353  elrspunidl  33399  elrspunsn  33400  drngidl  33404  mxidlmaxv  33439  mxidlirredi  33442  opprqusdrng  33464  qsdrnglem2  33467  rprmcl  33489  rprmirred  33502  pidufd  33514  1arithufdlem3  33517  dfufd2  33521  zringfrac  33525  ply1dg3rt0irred  33551  gsummoncoe1fzo  33563  lindsunlem  33620  fedgmullem1  33625  fedgmullem2  33626  assafld  33633  fldextrspunlsp  33669  irngnminplynz  33702  constrextdg2lem  33738  constrfiss  33741  constrsdrg  33765  submatminr1  33800  qtophaus  33826  qqhval2  33972  esummono  34044  gsumesum  34049  esum2dlem  34082  measvuni  34204  fiunelcarsg  34307  sitgclg  34333  sitgaddlemb  34339  eulerpartlemsv2  34349  eulerpartlemsv3  34352  eulerpartlemgc  34353  eulerpartlemv  34355  signstfvneq0  34563  signstfvcl  34564  signstfveq0a  34567  signstfveq0  34568  signsvfn  34573  signsvtp  34574  signsvtn  34575  signsvfpn  34576  signsvfnn  34577  signlem0  34578  hgt750leme  34649  onvf1odlem4  35093  iprodgam  35729  poimirlem2  37616  rrndstprj2  37825  lsatelbN  38999  lsatfixedN  39002  lkreqN  39163  lkrlspeqN  39164  dochnel2  41386  dochnel  41387  djhcvat42  41409  dochsnshp  41447  dochexmidat  41453  dochsnkr  41466  dochsnkr2  41467  dochsnkr2cl  41468  dochflcl  41469  dochfl1  41470  dochfln0  41471  lcfl6lem  41492  lcfl7lem  41493  lcfl8b  41498  lclkrlem2a  41501  lclkrlem2b  41502  lclkrlem2c  41503  lclkrlem2d  41504  lclkrlem2e  41505  lclkrlem2f  41506  lcfrlem14  41550  lcfrlem15  41551  lcfrlem16  41552  lcfrlem17  41553  lcfrlem18  41554  lcfrlem19  41555  lcfrlem20  41556  lcfrlem21  41557  lcfrlem23  41559  lcfrlem25  41561  lcfrlem26  41562  lcfrlem35  41571  lcfrlem36  41572  mapdn0  41663  mapdpglem29  41694  mapdpglem24  41698  baerlem3lem1  41701  baerlem5alem1  41702  baerlem5blem1  41703  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  baerlem5amN  41710  baerlem5bmN  41711  baerlem5abmN  41712  mapdindp0  41713  mapdindp1  41714  mapdindp2  41715  mapdindp3  41716  mapdindp4  41717  mapdheq2  41723  mapdheq4lem  41725  mapdheq4  41726  mapdh6lem1N  41727  mapdh6lem2N  41728  mapdh6aN  41729  mapdh6bN  41731  mapdh6cN  41732  mapdh6dN  41733  mapdh6eN  41734  mapdh6fN  41735  mapdh6gN  41736  mapdh6hN  41737  mapdh6iN  41738  mapdh7eN  41742  mapdh7cN  41743  mapdh7dN  41744  mapdh7fN  41745  mapdh75e  41746  mapdh75fN  41749  hvmaplfl  41761  mapdhvmap  41763  mapdh8aa  41770  mapdh8ab  41771  mapdh8ad  41773  mapdh8b  41774  mapdh8c  41775  mapdh8d0N  41776  mapdh8d  41777  mapdh8e  41778  mapdh9a  41783  mapdh9aOLDN  41784  hdmap1val2  41794  hdmap1eq  41795  hdmap1valc  41797  hdmap1eq2  41799  hdmap1eq4N  41800  hdmap1l6lem1  41801  hdmap1l6lem2  41802  hdmap1l6a  41803  hdmap1l6b  41805  hdmap1l6c  41806  hdmap1l6d  41807  hdmap1l6e  41808  hdmap1l6f  41809  hdmap1l6g  41810  hdmap1l6h  41811  hdmap1l6i  41812  hdmap1eulem  41816  hdmap1eulemOLDN  41817  hdmapcl  41824  hdmapval2lem  41825  hdmapval0  41827  hdmapeveclem  41828  hdmapevec  41829  hdmapval3lemN  41831  hdmapval3N  41832  hdmap10lem  41833  hdmap11lem1  41835  hdmap11lem2  41836  hdmapnzcl  41839  hdmaprnlem3N  41844  hdmaprnlem3uN  41845  hdmaprnlem4N  41847  hdmaprnlem7N  41849  hdmaprnlem8N  41850  hdmaprnlem9N  41851  hdmaprnlem3eN  41852  hdmaprnlem16N  41856  hdmap14lem1  41862  hdmap14lem2N  41863  hdmap14lem3  41864  hdmap14lem4a  41865  hdmap14lem6  41867  hdmap14lem8  41869  hdmap14lem9  41870  hdmap14lem10  41871  hdmap14lem11  41872  hdmap14lem12  41873  hgmaprnlem1N  41890  hgmaprnlem2N  41891  hgmaprnlem3N  41892  hgmaprnlem4N  41893  hdmapip1  41910  hdmapinvlem1  41912  hdmapinvlem2  41913  hdmapinvlem3  41914  hdmapinvlem4  41915  hdmapglem5  41916  hgmapvvlem1  41917  hgmapvvlem2  41918  hgmapvvlem3  41919  hdmapglem7a  41921  hdmapglem7b  41922  hdmapglem7  41923  evl1gprodd  42105  nelsubginvcld  42484  nelsubgcld  42485  nelsubgsubcld  42486  domnexpgn0cl  42511  fidomncyc  42523  prjspnfv01  42612  prjspner01  42613  prjspner1  42614  dffltz  42622  qirropth  42896  rmxyneg  42909  rmxm1  42923  rmxluc  42925  rmxdbl  42928  ltrmxnn0  42938  jm2.19lem1  42978  jm2.23  42985  rmxdiophlem  43004  aomclem2  43044  cantnftermord  43309  inaex  44286  bccm1k  44331  dstregt0  45280  fprodexp  45592  fprodabs2  45593  mccllem  45595  fprodcnlem  45597  climrec  45601  climdivf  45610  islpcn  45637  lptre2pt  45638  0ellimcdiv  45647  reclimc  45651  divlimc  45654  cncficcgt0  45886  dvdivf  45920  stoweidlem34  46032  stoweidlem43  46041  etransclem46  46278  etransclem47  46279  etransclem48  46280  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmvlelem3  46595  hoidmvlelem4  46596  hspdifhsp  46614  readdcnnred  47304  resubcnnred  47305  recnmulnred  47306  cndivrenred  47307