Theorem eldifad 3911

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902

This theorem is used by:  xpdifid  6160  xpdifcnvepel  6161  fvdifsupp  8170  unblem1  9265  cantnflem3  9673  cantnflem4  9674  oef1o  9680  infxpenc  10024  acndom2  10060  ackbij1lem18  10241  infpssrlem3  10310  fin23lem26  10330  fin23lem30  10347  pwfseqlem4a  10673  elfzodif0  13829  expclz  14151  pfxchn  18701  chnind  18712  chnccats1  18716  chnccat  18717  symgextf  19547  pmtrfinv  19591  symggen  19600  efgsdmi  19862  efgs1b  19866  efgsp1  19867  efgsres  19868  efgredlemf  19871  efgredlemd  19874  efgredlemc  19875  efgredlem  19877  efgrelexlemb  19880  gsum2d2lem  20103  pgpfac1lem2  20207  pgpfac1lem3a  20208  pgpfac1lem3  20209  pgpfac1lem4  20210  zrzeroorngc  20809  zrtermoringc  20840  zrninitoringc  20841  domneq0r  20888  isdrng4  20905  isdrng2  20909  fidomndrnglem  20942  lvecinv  21303  lspsncmp  21306  lspsnne1  21307  lspsnnecom  21309  lspabs2  21310  lspsneu  21313  lspdisjb  21316  lspexch  21319  lspindp1  21323  lvecindp2  21329  lspsolv  21333  lspsnat  21335  lsppratlem1  21337  lsppratlem2  21338  drngidl  21451  prmidlsubm  21553  nzerooringczr  21696  frlmssuvc2  22011  evls1fpws  22597  maducoeval2  22865  hauscmplem  23634  1stccnp  23691  imasdsf1olem  24602  rrxmetlem  25638  divcncf  25678  dvrec  26185  dvmptdiv  26204  ftc1lem6  26271  elqaalem1  26554  elqaalem3  26556  ulmdvlem3  26641  abelthlem6  26675  abelthlem7a  26676  abelthlem7  26677  logtayl  26900  dmgmn0  27265  dmgmaddnn0  27266  dmgmdivn0  27267  lgamgulmlem2  27269  lgamgulmlem3  27270  lgamgulmlem5  27272  lgamgulmlem6  27273  lgamgulm2  27275  lgambdd  27276  lgamucov  27277  lgamcvg2  27294  gamcvg  27295  gamcvg2lem  27298  ftalem3  27314  lgsqrlem1  27585  lgsqrlem2  27586  lgsqrlem3  27587  lgsqrlem4  27588  lgseisenlem1  27614  lgseisenlem2  27615  lgseisenlem3  27616  lgseisenlem4  27617  lgseisen  27618  lgsquadlem1  27619  lgsquadlem2  27620  lgsquadlem3  27621  chebbnd1lem1  27708  dchrisum0re  27752  dchrisum0lema  27753  dchrisum0lem1b  27754  dchrisum0lem1  27755  dchrisum0lem2a  27756  dchrisum0lem2  27757  tgisline  28977  oppmir  29114  tgelrnpln  29136  elplng  29140  elplngid  29142  plngcplem  29145  plngrotlem1  29147  plngrotlem2  29148  plngrotlem3  29149  plngrot  29150  lnssplnglem  29151  lnssplng  29152  plngmiropp  29154  nhpmirhp  29158  ragsupplcgra  29227  perpeqlem  29229  angmgmaddlid  29274  angmgmaddrid  29275  angmgmlem  29277  dfprlng2  29307  perpprlng  29310  prlngex  29311  prlngmolem1  29312  prlngmolem2  29313  prlngeu  29315  prlngmid2  29321  elntg  29444  uhgrss  29524  upgrex  29552  edguhgr  29589  1loopgrvd0  29967  disjiunel  33072  suppovss  33156  nn0difffzod  33278  gsumfs2d  33504  gsumhashmul  33510  suppgsumssiun  33515  odpmco  33529  pmtrcnel  33532  pmtrcnelor  33534  cycpmco2f1  33567  cycpmco2rn  33568  cycpmco2lem1  33569  cycpmco2lem2  33570  cycpmco2lem3  33571  cycpmco2lem4  33572  cycpmco2lem5  33573  cycpmco2lem6  33574  cycpmco2lem7  33575  cycpmco2  33576  cyc3co2  33583  tocyccntz  33587  cyc3conja  33600  fxpsdrg  33618  elrgspnlem2  33686  elrgspnlem4  33688  elrgspnsubrunlem2  33691  domnprodn0  33721  domnprodeq0  33722  fracfld  33752  lindssn  33814  lindfpropd  33818  elrspunidl  33859  elrspunsn  33860  mxidlmaxv  33874  mxidlirredi  33877  opprqusdrng  33898  qsdrnglem2  33901  dflringlem  33907  dflringlem2  33908  rprmcl  33931  rprmirred  33944  pidufd  33956  1arithufdlem3  33959  dfufd2  33963  zringfrac  33967  deg1prod  33996  ply1dg3rt0irred  33997  gsummoncoe1fzo  34010  mplvrpmrhm  34060  psrgsum  34061  psrmonprod  34065  esplyfval2  34078  lindsunlem  34137  fedgmullem1  34142  fedgmullem2  34143  assafld  34150  fldextrspunlsp  34187  extdgfialglem2  34206  irngnminplynz  34225  constrextdg2lem  34261  constrfiss  34264  constrsdrg  34288  submatminr1  34323  qtophaus  34349  qqhval2  34495  esummono  34567  gsumesum  34572  esum2dlem  34605  measvuni  34728  fiunelcarsg  34830  sitgclg  34856  sitgaddlemb  34862  eulerpartlemsv2  34872  eulerpartlemsv3  34875  eulerpartlemgc  34876  eulerpartlemv  34878  signstfvneq0  35083  signstfvcl  35084  signstfveq0a  35087  signstfveq0  35088  signsvfn  35093  signsvtp  35094  signsvtn  35095  signsvfpn  35096  signsvfnn  35097  signlem0  35098  hgt750leme  35169  onvf1odlem4  35706  iprodgam  36324  ttcwf2  37147  mh-inf3f1  37163  poimirlem2  38374  rrndstprj2  38584  lsatelbN  39882  lsatfixedN  39885  lkreqN  40046  lkrlspeqN  40047  dochnel2  42268  dochnel  42269  djhcvat42  42291  dochsnshp  42329  dochexmidat  42335  dochsnkr  42348  dochsnkr2  42349  dochsnkr2cl  42350  dochflcl  42351  dochfl1  42352  dochfln0  42353  lcfl6lem  42374  lcfl7lem  42375  lcfl8b  42380  lclkrlem2a  42383  lclkrlem2b  42384  lclkrlem2c  42385  lclkrlem2d  42386  lclkrlem2e  42387  lclkrlem2f  42388  lcfrlem14  42432  lcfrlem15  42433  lcfrlem16  42434  lcfrlem17  42435  lcfrlem18  42436  lcfrlem19  42437  lcfrlem20  42438  lcfrlem21  42439  lcfrlem23  42441  lcfrlem25  42443  lcfrlem26  42444  lcfrlem35  42453  lcfrlem36  42454  mapdn0  42545  mapdpglem29  42576  mapdpglem24  42580  baerlem3lem1  42583  baerlem5alem1  42584  baerlem5blem1  42585  baerlem3lem2  42586  baerlem5alem2  42587  baerlem5blem2  42588  baerlem5amN  42592  baerlem5bmN  42593  baerlem5abmN  42594  mapdindp0  42595  mapdindp1  42596  mapdindp2  42597  mapdindp3  42598  mapdindp4  42599  mapdheq2  42605  mapdheq4lem  42607  mapdheq4  42608  mapdh6lem1N  42609  mapdh6lem2N  42610  mapdh6aN  42611  mapdh6bN  42613  mapdh6cN  42614  mapdh6dN  42615  mapdh6eN  42616  mapdh6fN  42617  mapdh6gN  42618  mapdh6hN  42619  mapdh6iN  42620  mapdh7eN  42624  mapdh7cN  42625  mapdh7dN  42626  mapdh7fN  42627  mapdh75e  42628  mapdh75fN  42631  hvmaplfl  42643  mapdhvmap  42645  mapdh8aa  42652  mapdh8ab  42653  mapdh8ad  42655  mapdh8b  42656  mapdh8c  42657  mapdh8d0N  42658  mapdh8d  42659  mapdh8e  42660  mapdh9a  42665  mapdh9aOLDN  42666  hdmap1val2  42676  hdmap1eq  42677  hdmap1valc  42679  hdmap1eq2  42681  hdmap1eq4N  42682  hdmap1l6lem1  42683  hdmap1l6lem2  42684  hdmap1l6a  42685  hdmap1l6b  42687  hdmap1l6c  42688  hdmap1l6d  42689  hdmap1l6e  42690  hdmap1l6f  42691  hdmap1l6g  42692  hdmap1l6h  42693  hdmap1l6i  42694  hdmap1eulem  42698  hdmap1eulemOLDN  42699  hdmapcl  42706  hdmapval2lem  42707  hdmapval0  42709  hdmapeveclem  42710  hdmapevec  42711  hdmapval3lemN  42713  hdmapval3N  42714  hdmap10lem  42715  hdmap11lem1  42717  hdmap11lem2  42718  hdmapnzcl  42721  hdmaprnlem3N  42726  hdmaprnlem3uN  42727  hdmaprnlem4N  42729  hdmaprnlem7N  42731  hdmaprnlem8N  42732  hdmaprnlem9N  42733  hdmaprnlem3eN  42734  hdmaprnlem16N  42738  hdmap14lem1  42744  hdmap14lem2N  42745  hdmap14lem3  42746  hdmap14lem4a  42747  hdmap14lem6  42749  hdmap14lem8  42751  hdmap14lem9  42752  hdmap14lem10  42753  hdmap14lem11  42754  hdmap14lem12  42755  hgmaprnlem1N  42772  hgmaprnlem2N  42773  hgmaprnlem3N  42774  hgmaprnlem4N  42775  hdmapip1  42792  hdmapinvlem1  42794  hdmapinvlem2  42795  hdmapinvlem3  42796  hdmapinvlem4  42797  hdmapglem5  42798  hgmapvvlem1  42799  hgmapvvlem2  42800  hgmapvvlem3  42801  hdmapglem7a  42803  hdmapglem7b  42804  hdmapglem7  42805  evl1gprodd  42986  nelsubginvcld  43387  nelsubgcld  43388  nelsubgsubcld  43389  domnexpgn0cl  43408  fidomncyc  43420  prjspnfv01  43473  prjspner01  43474  prjspner1  43475  dffltz  43483  qirropth  43752  rmxyneg  43764  rmxm1  43778  rmxluc  43780  rmxdbl  43783  ltrmxnn0  43793  jm2.19lem1  43833  jm2.23  43840  rmxdiophlem  43859  aomclem2  43899  cantnftermord  44164  inaex  45124  bccm1k  45169  dstregt0  46118  fprodexp  46427  fprodabs2  46428  mccllem  46430  fprodcnlem  46432  climrec  46436  climdivf  46445  islpcn  46470  lptre2pt  46471  0ellimcdiv  46480  reclimc  46484  divlimc  46487  cncficcgt0  46719  dvdivf  46753  stoweidlem34  46865  stoweidlem43  46874  etransclem46  47111  etransclem47  47112  etransclem48  47113  hsphoidmvle2  47416  hsphoidmvle  47417  hoidmvlelem3  47428  hoidmvlelem4  47429  hspdifhsp  47447  readdcnnred  48194  resubcnnred  48195  recnmulnred  48196  cndivrenred  48197