Theorem eldifad 3959

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2106   ∖ cdif 3944

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950

This theorem is referenced by:  xpdifid  6164  unblem1  9291  cantnflem3  9682  cantnflem4  9683  oef1o  9689  infxpenc  10009  acndom2  10045  ackbij1lem18  10228  infpssrlem3  10296  fin23lem26  10316  fin23lem30  10333  pwfseqlem4a  10652  expclz  14046  symgextf  19279  pmtrfinv  19323  symggen  19332  efgsdmi  19594  efgs1b  19598  efgsp1  19599  efgsres  19600  efgredlemf  19603  efgredlemd  19606  efgredlemc  19607  efgredlem  19609  efgrelexlemb  19612  gsum2d2lem  19835  pgpfac1lem2  19939  pgpfac1lem3a  19940  pgpfac1lem3  19941  pgpfac1lem4  19942  isdrng2  20321  lvecinv  20718  lspsncmp  20721  lspsnne1  20722  lspsnnecom  20724  lspabs2  20725  lspsneu  20728  lspdisjb  20731  lspexch  20734  lspindp1  20738  lvecindp2  20744  lspsolv  20748  lspsnat  20750  lsppratlem1  20752  lsppratlem2  20753  fidomndrnglem  20917  frlmssuvc2  21341  maducoeval2  22133  hauscmplem  22901  1stccnp  22957  imasdsf1olem  23870  rrxmetlem  24915  divcncf  24955  dvrec  25463  dvmptdiv  25482  ftc1lem6  25549  elqaalem1  25823  elqaalem3  25825  ulmdvlem3  25905  abelthlem6  25939  abelthlem7a  25940  abelthlem7  25941  logtayl  26159  dmgmn0  26519  dmgmaddnn0  26520  dmgmdivn0  26521  lgamgulmlem2  26523  lgamgulmlem3  26524  lgamgulmlem5  26526  lgamgulmlem6  26527  lgamgulm2  26529  lgambdd  26530  lgamucov  26531  lgamcvg2  26548  gamcvg  26549  gamcvg2lem  26552  ftalem3  26568  lgsqrlem1  26838  lgsqrlem2  26839  lgsqrlem3  26840  lgsqrlem4  26841  lgseisenlem1  26867  lgseisenlem2  26868  lgseisenlem3  26869  lgseisenlem4  26870  lgseisen  26871  lgsquadlem1  26872  lgsquadlem2  26873  lgsquadlem3  26874  chebbnd1lem1  26961  dchrisum0re  27005  dchrisum0lema  27006  dchrisum0lem1b  27007  dchrisum0lem1  27008  dchrisum0lem2a  27009  dchrisum0lem2  27010  tgisline  27867  elntg  28231  uhgrss  28313  upgrex  28341  edguhgr  28378  1loopgrvd0  28750  disjiunel  31814  suppovss  31893  fvdifsupp  31894  nn0difffzod  32003  gsumhashmul  32195  odpmco  32234  pmtrcnel  32237  pmtrcnelor  32239  cycpmco2f1  32270  cycpmco2rn  32271  cycpmco2lem1  32272  cycpmco2lem2  32273  cycpmco2lem3  32274  cycpmco2lem4  32275  cycpmco2lem5  32276  cycpmco2lem6  32277  cycpmco2lem7  32278  cycpmco2  32279  cyc3co2  32286  tocyccntz  32290  cyc3conja  32303  idomrcan  32364  isdrng4  32383  lindssn  32482  lindfpropd  32486  elrspunidl  32534  elrspunsn  32535  drngidl  32539  mxidlmaxv  32572  mxidlirredi  32575  opprqusdrng  32595  qsdrnglem2  32598  evls1fpws  32634  gsummoncoe1fzo  32656  lindsunlem  32697  fedgmullem1  32702  fedgmullem2  32703  irngnminplynz  32759  submatminr1  32778  qtophaus  32804  qqhval2  32950  esummono  33040  gsumesum  33045  esum2dlem  33078  measvuni  33200  fiunelcarsg  33303  sitgclg  33329  sitgaddlemb  33335  eulerpartlemsv2  33345  eulerpartlemsv3  33348  eulerpartlemgc  33349  eulerpartlemv  33351  signstfvneq0  33571  signstfvcl  33572  signstfveq0a  33575  signstfveq0  33576  signsvfn  33581  signsvtp  33582  signsvtn  33583  signsvfpn  33584  signsvfnn  33585  signlem0  33586  hgt750leme  33658  iprodgam  34700  poimirlem2  36478  rrndstprj2  36687  lsatelbN  37864  lsatfixedN  37867  lkreqN  38028  lkrlspeqN  38029  dochnel2  40251  dochnel  40252  djhcvat42  40274  dochsnshp  40312  dochexmidat  40318  dochsnkr  40331  dochsnkr2  40332  dochsnkr2cl  40333  dochflcl  40334  dochfl1  40335  dochfln0  40336  lcfl6lem  40357  lcfl7lem  40358  lcfl8b  40363  lclkrlem2a  40366  lclkrlem2b  40367  lclkrlem2c  40368  lclkrlem2d  40369  lclkrlem2e  40370  lclkrlem2f  40371  lcfrlem14  40415  lcfrlem15  40416  lcfrlem16  40417  lcfrlem17  40418  lcfrlem18  40419  lcfrlem19  40420  lcfrlem20  40421  lcfrlem21  40422  lcfrlem23  40424  lcfrlem25  40426  lcfrlem26  40427  lcfrlem35  40436  lcfrlem36  40437  mapdn0  40528  mapdpglem29  40559  mapdpglem24  40563  baerlem3lem1  40566  baerlem5alem1  40567  baerlem5blem1  40568  baerlem3lem2  40569  baerlem5alem2  40570  baerlem5blem2  40571  baerlem5amN  40575  baerlem5bmN  40576  baerlem5abmN  40577  mapdindp0  40578  mapdindp1  40579  mapdindp2  40580  mapdindp3  40581  mapdindp4  40582  mapdheq2  40588  mapdheq4lem  40590  mapdheq4  40591  mapdh6lem1N  40592  mapdh6lem2N  40593  mapdh6aN  40594  mapdh6bN  40596  mapdh6cN  40597  mapdh6dN  40598  mapdh6eN  40599  mapdh6fN  40600  mapdh6gN  40601  mapdh6hN  40602  mapdh6iN  40603  mapdh7eN  40607  mapdh7cN  40608  mapdh7dN  40609  mapdh7fN  40610  mapdh75e  40611  mapdh75fN  40614  hvmaplfl  40626  mapdhvmap  40628  mapdh8aa  40635  mapdh8ab  40636  mapdh8ad  40638  mapdh8b  40639  mapdh8c  40640  mapdh8d0N  40641  mapdh8d  40642  mapdh8e  40643  mapdh9a  40648  mapdh9aOLDN  40649  hdmap1val2  40659  hdmap1eq  40660  hdmap1valc  40662  hdmap1eq2  40664  hdmap1eq4N  40665  hdmap1l6lem1  40666  hdmap1l6lem2  40667  hdmap1l6a  40668  hdmap1l6b  40670  hdmap1l6c  40671  hdmap1l6d  40672  hdmap1l6e  40673  hdmap1l6f  40674  hdmap1l6g  40675  hdmap1l6h  40676  hdmap1l6i  40677  hdmap1eulem  40681  hdmap1eulemOLDN  40682  hdmapcl  40689  hdmapval2lem  40690  hdmapval0  40692  hdmapeveclem  40693  hdmapevec  40694  hdmapval3lemN  40696  hdmapval3N  40697  hdmap10lem  40698  hdmap11lem1  40700  hdmap11lem2  40701  hdmapnzcl  40704  hdmaprnlem3N  40709  hdmaprnlem3uN  40710  hdmaprnlem4N  40712  hdmaprnlem7N  40714  hdmaprnlem8N  40715  hdmaprnlem9N  40716  hdmaprnlem3eN  40717  hdmaprnlem16N  40721  hdmap14lem1  40727  hdmap14lem2N  40728  hdmap14lem3  40729  hdmap14lem4a  40730  hdmap14lem6  40732  hdmap14lem8  40734  hdmap14lem9  40735  hdmap14lem10  40736  hdmap14lem11  40737  hdmap14lem12  40738  hgmaprnlem1N  40755  hgmaprnlem2N  40756  hgmaprnlem3N  40757  hgmaprnlem4N  40758  hdmapip1  40775  hdmapinvlem1  40777  hdmapinvlem2  40778  hdmapinvlem3  40779  hdmapinvlem4  40780  hdmapglem5  40781  hgmapvvlem1  40782  hgmapvvlem2  40783  hgmapvvlem3  40784  hdmapglem7a  40786  hdmapglem7b  40787  hdmapglem7  40788  nelsubginvcld  41067  nelsubgcld  41068  nelsubgsubcld  41069  prjspnfv01  41362  prjspner01  41363  prjspner1  41364  dffltz  41372  qirropth  41631  rmxyneg  41644  rmxm1  41658  rmxluc  41660  rmxdbl  41663  ltrmxnn0  41673  jm2.19lem1  41713  jm2.23  41720  rmxdiophlem  41739  aomclem2  41782  cantnftermord  42055  inaex  43041  bccm1k  43086  dstregt0  43977  fprodexp  44296  fprodabs2  44297  mccllem  44299  fprodcnlem  44301  climrec  44305  climdivf  44314  islpcn  44341  lptre2pt  44342  0ellimcdiv  44351  reclimc  44355  divlimc  44358  cncficcgt0  44590  dvdivf  44624  stoweidlem34  44736  stoweidlem43  44745  etransclem46  44982  etransclem47  44983  etransclem48  44984  hsphoidmvle2  45287  hsphoidmvle  45288  hoidmvlelem3  45299  hoidmvlelem4  45300  hspdifhsp  45318  readdcnnred  45997  resubcnnred  45998  recnmulnred  45999  cndivrenred  46000  zrzeroorngc  46853  zrtermoringc  46921  zrninitoringc  46922  nzerooringczr  46923