Theorem eldifad 3917

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2143   ∖ cdif 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908

This theorem is referenced by:  xpdifid  6165  xpdifcnvepel  6166  fvdifsupp  8163  unblem1  9248  cantnflem3  9656  cantnflem4  9657  oef1o  9663  infxpenc  9998  acndom2  10034  ackbij1lem18  10215  infpssrlem3  10284  fin23lem26  10304  fin23lem30  10321  pwfseqlem4a  10641  elfzodif0  13795  expclz  14116  pfxchn  18661  chnind  18672  chnccats1  18676  chnccat  18677  symgextf  19482  pmtrfinv  19526  symggen  19535  efgsdmi  19797  efgs1b  19801  efgsp1  19802  efgsres  19803  efgredlemf  19806  efgredlemd  19809  efgredlemc  19810  efgredlem  19812  efgrelexlemb  19815  gsum2d2lem  20038  pgpfac1lem2  20142  pgpfac1lem3a  20143  pgpfac1lem3  20144  pgpfac1lem4  20145  zrzeroorngc  20743  zrtermoringc  20774  zrninitoringc  20775  domneq0r  20822  isdrng4  20839  isdrng2  20843  fidomndrnglem  20876  lvecinv  21237  lspsncmp  21240  lspsnne1  21241  lspsnnecom  21243  lspabs2  21244  lspsneu  21247  lspdisjb  21250  lspexch  21253  lspindp1  21257  lvecindp2  21263  lspsolv  21267  lspsnat  21269  lsppratlem1  21271  lsppratlem2  21272  drngidl  21385  prmidlsubm  21487  nzerooringczr  21630  frlmssuvc2  21945  evls1fpws  22529  maducoeval2  22797  hauscmplem  23563  1stccnp  23619  imasdsf1olem  24530  rrxmetlem  25566  divcncf  25606  dvrec  26114  dvmptdiv  26133  ftc1lem6  26200  elqaalem1  26480  elqaalem3  26482  ulmdvlem3  26565  abelthlem6  26599  abelthlem7a  26600  abelthlem7  26601  logtayl  26825  dmgmn0  27190  dmgmaddnn0  27191  dmgmdivn0  27192  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem5  27197  lgamgulmlem6  27198  lgamgulm2  27200  lgambdd  27201  lgamucov  27202  lgamcvg2  27219  gamcvg  27220  gamcvg2lem  27223  ftalem3  27239  lgsqrlem1  27510  lgsqrlem2  27511  lgsqrlem3  27512  lgsqrlem4  27513  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgseisenlem4  27542  lgseisen  27543  lgsquadlem1  27544  lgsquadlem2  27545  lgsquadlem3  27546  chebbnd1lem1  27633  dchrisum0re  27677  dchrisum0lema  27678  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0lem2  27682  tgisline  28900  oppmir  29036  tgelrnpln  29058  elplng  29062  elplngid  29064  plngcplem  29067  plngrotlem1  29069  plngrotlem2  29070  plngrotlem3  29071  plngrot  29072  lnssplnglem  29073  lnssplng  29074  plngmiropp  29076  nhpmirhp  29080  ragsupplcgra  29148  perpeqlem  29150  dfprlng2  29197  perpprlng  29200  prlngex  29201  prlngmolem1  29202  prlngmolem2  29203  prlngeu  29205  prlngmid2  29211  elntg  29334  uhgrss  29414  upgrex  29442  edguhgr  29479  1loopgrvd0  29854  disjiunel  32941  suppovss  33026  nn0difffzod  33149  gsumfs2d  33381  gsumhashmul  33387  suppgsumssiun  33392  odpmco  33406  pmtrcnel  33409  pmtrcnelor  33411  cycpmco2f1  33444  cycpmco2rn  33445  cycpmco2lem1  33446  cycpmco2lem2  33447  cycpmco2lem3  33448  cycpmco2lem4  33449  cycpmco2lem5  33450  cycpmco2lem6  33451  cycpmco2lem7  33452  cycpmco2  33453  cyc3co2  33460  tocyccntz  33464  cyc3conja  33477  fxpsdrg  33495  elrgspnlem2  33563  elrgspnlem4  33565  elrgspnsubrunlem2  33568  domnprodn0  33598  domnprodeq0  33599  fracfld  33629  lindssn  33691  lindfpropd  33695  elrspunidl  33736  elrspunsn  33737  mxidlmaxv  33751  mxidlirredi  33754  opprqusdrng  33775  qsdrnglem2  33778  dflringlem  33784  dflringlem2  33785  rprmcl  33808  rprmirred  33821  pidufd  33833  1arithufdlem3  33836  dfufd2  33840  zringfrac  33844  deg1prod  33873  ply1dg3rt0irred  33874  gsummoncoe1fzo  33887  mplvrpmrhm  33937  psrgsum  33938  psrmonprod  33942  esplyfval2  33955  lindsunlem  34014  fedgmullem1  34019  fedgmullem2  34020  assafld  34027  fldextrspunlsp  34064  extdgfialglem2  34083  irngnminplynz  34102  constrextdg2lem  34138  constrfiss  34141  constrsdrg  34165  submatminr1  34200  qtophaus  34226  qqhval2  34372  esummono  34444  gsumesum  34449  esum2dlem  34482  measvuni  34604  fiunelcarsg  34706  sitgclg  34732  sitgaddlemb  34738  eulerpartlemsv2  34748  eulerpartlemsv3  34751  eulerpartlemgc  34752  eulerpartlemv  34754  signstfvneq0  34959  signstfvcl  34960  signstfveq0a  34963  signstfveq0  34964  signsvfn  34969  signsvtp  34970  signsvtn  34971  signsvfpn  34972  signsvfnn  34973  signlem0  34974  hgt750leme  35045  onvf1odlem4  35590  iprodgam  36234  ttcwf2  37056  mh-inf3f1  37072  poimirlem2  38293  rrndstprj2  38502  lsatelbN  39800  lsatfixedN  39803  lkreqN  39964  lkrlspeqN  39965  dochnel2  42186  dochnel  42187  djhcvat42  42209  dochsnshp  42247  dochexmidat  42253  dochsnkr  42266  dochsnkr2  42267  dochsnkr2cl  42268  dochflcl  42269  dochfl1  42270  dochfln0  42271  lcfl6lem  42292  lcfl7lem  42293  lcfl8b  42298  lclkrlem2a  42301  lclkrlem2b  42302  lclkrlem2c  42303  lclkrlem2d  42304  lclkrlem2e  42305  lclkrlem2f  42306  lcfrlem14  42350  lcfrlem15  42351  lcfrlem16  42352  lcfrlem17  42353  lcfrlem18  42354  lcfrlem19  42355  lcfrlem20  42356  lcfrlem21  42357  lcfrlem23  42359  lcfrlem25  42361  lcfrlem26  42362  lcfrlem35  42371  lcfrlem36  42372  mapdn0  42463  mapdpglem29  42494  mapdpglem24  42498  baerlem3lem1  42501  baerlem5alem1  42502  baerlem5blem1  42503  baerlem3lem2  42504  baerlem5alem2  42505  baerlem5blem2  42506  baerlem5amN  42510  baerlem5bmN  42511  baerlem5abmN  42512  mapdindp0  42513  mapdindp1  42514  mapdindp2  42515  mapdindp3  42516  mapdindp4  42517  mapdheq2  42523  mapdheq4lem  42525  mapdheq4  42526  mapdh6lem1N  42527  mapdh6lem2N  42528  mapdh6aN  42529  mapdh6bN  42531  mapdh6cN  42532  mapdh6dN  42533  mapdh6eN  42534  mapdh6fN  42535  mapdh6gN  42536  mapdh6hN  42537  mapdh6iN  42538  mapdh7eN  42542  mapdh7cN  42543  mapdh7dN  42544  mapdh7fN  42545  mapdh75e  42546  mapdh75fN  42549  hvmaplfl  42561  mapdhvmap  42563  mapdh8aa  42570  mapdh8ab  42571  mapdh8ad  42573  mapdh8b  42574  mapdh8c  42575  mapdh8d0N  42576  mapdh8d  42577  mapdh8e  42578  mapdh9a  42583  mapdh9aOLDN  42584  hdmap1val2  42594  hdmap1eq  42595  hdmap1valc  42597  hdmap1eq2  42599  hdmap1eq4N  42600  hdmap1l6lem1  42601  hdmap1l6lem2  42602  hdmap1l6a  42603  hdmap1l6b  42605  hdmap1l6c  42606  hdmap1l6d  42607  hdmap1l6e  42608  hdmap1l6f  42609  hdmap1l6g  42610  hdmap1l6h  42611  hdmap1l6i  42612  hdmap1eulem  42616  hdmap1eulemOLDN  42617  hdmapcl  42624  hdmapval2lem  42625  hdmapval0  42627  hdmapeveclem  42628  hdmapevec  42629  hdmapval3lemN  42631  hdmapval3N  42632  hdmap10lem  42633  hdmap11lem1  42635  hdmap11lem2  42636  hdmapnzcl  42639  hdmaprnlem3N  42644  hdmaprnlem3uN  42645  hdmaprnlem4N  42647  hdmaprnlem7N  42649  hdmaprnlem8N  42650  hdmaprnlem9N  42651  hdmaprnlem3eN  42652  hdmaprnlem16N  42656  hdmap14lem1  42662  hdmap14lem2N  42663  hdmap14lem3  42664  hdmap14lem4a  42665  hdmap14lem6  42667  hdmap14lem8  42669  hdmap14lem9  42670  hdmap14lem10  42671  hdmap14lem11  42672  hdmap14lem12  42673  hgmaprnlem1N  42690  hgmaprnlem2N  42691  hgmaprnlem3N  42692  hgmaprnlem4N  42693  hdmapip1  42710  hdmapinvlem1  42712  hdmapinvlem2  42713  hdmapinvlem3  42714  hdmapinvlem4  42715  hdmapglem5  42716  hgmapvvlem1  42717  hgmapvvlem2  42718  hgmapvvlem3  42719  hdmapglem7a  42721  hdmapglem7b  42722  hdmapglem7  42723  evl1gprodd  42904  nelsubginvcld  43290  nelsubgcld  43291  nelsubgsubcld  43292  domnexpgn0cl  43311  fidomncyc  43323  prjspnfv01  43376  prjspner01  43377  prjspner1  43378  dffltz  43386  qirropth  43655  rmxyneg  43667  rmxm1  43681  rmxluc  43683  rmxdbl  43686  ltrmxnn0  43696  jm2.19lem1  43736  jm2.23  43743  rmxdiophlem  43762  aomclem2  43802  cantnftermord  44067  inaex  45027  bccm1k  45072  dstregt0  46021  fprodexp  46330  fprodabs2  46331  mccllem  46333  fprodcnlem  46335  climrec  46339  climdivf  46348  islpcn  46373  lptre2pt  46374  0ellimcdiv  46383  reclimc  46387  divlimc  46390  cncficcgt0  46622  dvdivf  46656  stoweidlem34  46768  stoweidlem43  46777  etransclem46  47014  etransclem47  47015  etransclem48  47016  hsphoidmvle2  47319  hsphoidmvle  47320  hoidmvlelem3  47331  hoidmvlelem4  47332  hspdifhsp  47350  readdcnnred  48060  resubcnnred  48061  recnmulnred  48062  cndivrenred  48063