Theorem eldifad 4054

Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 4052. (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 4052	. . 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 2146   ∖ cdif 4048

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050

This theorem is used by:  xpdifid  6165  xpdifcnvepel  6166  fvdifsupp  8202  unblem1  9298  cantnflem3  9705  cantnflem4  9706  oef1o  9712  infxpenc  10110  acndom2  10146  ackbij1lem18  10327  infpssrlem3  10396  fin23lem26  10416  fin23lem30  10433  pwfseqlem4a  10759  elfzodif0  13918  expclz  14240  pfxchn  18799  chnind  18810  chnccats1  18814  chnccat  18815  symgextf  19646  pmtrfinv  19690  symggen  19699  efgsdmi  19961  efgs1b  19965  efgsp1  19966  efgsres  19967  efgredlemf  19970  efgredlemd  19973  efgredlemc  19974  efgredlem  19976  efgrelexlemb  19979  gsum2d2lem  20202  pgpfac1lem2  20306  pgpfac1lem3a  20307  pgpfac1lem3  20308  pgpfac1lem4  20309  zrzeroorngc  20911  zrtermoringc  20942  zrninitoringc  20943  domneq0r  20990  isdrng4  21007  isdrng2  21012  fidomndrnglem  21045  lvecinv  21406  lspsncmp  21409  lspsnne1  21410  lspsnnecom  21412  lspabs2  21413  lspsneu  21416  lspdisjb  21419  lspexch  21422  lspindp1  21426  lvecindp2  21432  lspsolv  21436  lspsnat  21438  lsppratlem1  21440  lsppratlem2  21441  drngidl  21554  prmidlsubm  21658  nzerooringczr  21801  frlmssuvc2  22116  evls1fpws  22702  maducoeval2  22970  hauscmplem  23739  1stccnp  23796  imasdsf1olem  24707  rrxmetlem  25743  divcncf  25783  dvrec  26290  dvmptdiv  26309  ftc1lem6  26376  elqaalem1  26657  elqaalem3  26659  ulmdvlem3  26744  abelthlem6  26778  abelthlem7a  26779  abelthlem7  26780  logtayl  27003  dmgmn0  27368  dmgmaddnn0  27369  dmgmdivn0  27370  lgamgulmlem2  27372  lgamgulmlem3  27373  lgamgulmlem5  27375  lgamgulmlem6  27376  lgamgulm2  27378  lgambdd  27379  lgamucov  27380  lgamcvg2  27397  gamcvg  27398  gamcvg2lem  27401  ftalem3  27417  lgsqrlem1  27688  lgsqrlem2  27689  lgsqrlem3  27690  lgsqrlem4  27691  lgseisenlem1  27717  lgseisenlem2  27718  lgseisenlem3  27719  lgseisenlem4  27720  lgseisen  27721  lgsquadlem1  27722  lgsquadlem2  27723  lgsquadlem3  27724  chebbnd1lem1  27811  dchrisum0re  27855  dchrisum0lema  27856  dchrisum0lem1b  27857  dchrisum0lem1  27858  dchrisum0lem2a  27859  dchrisum0lem2  27860  tgisline  29110  oppmir  29247  tgelrnpln  29269  elplng  29273  elplngid  29275  plngcplem  29278  plngrotlem1  29280  plngrotlem2  29281  plngrotlem3  29282  plngrot  29283  lnssplnglem  29284  lnssplng  29285  plngmiropp  29287  nhpmirhp  29291  ragsupplcgra  29360  perpeqlem  29362  angmgmaddlid  29407  angmgmaddrid  29408  angmgmlem  29410  dfprlng2  29440  perpprlng  29443  prlngex  29444  prlngmolem1  29445  prlngmolem2  29446  prlngeu  29448  prlngmid2  29454  elntg  29577  uhgrss  29657  upgrex  29685  edguhgr  29722  1loopgrvd0  30100  disjiunel  33247  suppovss  33331  nn0difffzod  33452  gsumfs2d  33678  gsumhashmul  33684  suppgsumssiun  33689  odpmco  33703  pmtrcnel  33706  pmtrcnelor  33708  cycpmco2f1  33741  cycpmco2rn  33742  cycpmco2lem1  33743  cycpmco2lem2  33744  cycpmco2lem3  33745  cycpmco2lem4  33746  cycpmco2lem5  33747  cycpmco2lem6  33748  cycpmco2lem7  33749  cycpmco2  33750  cyc3co2  33757  tocyccntz  33761  cyc3conja  33774  fxpsdrg  33792  elrgspnlem2  33860  elrgspnlem4  33862  elrgspnsubrunlem2  33865  domnprodn0  33895  domnprodeq0  33896  fracfld  33926  lindssn  33989  lindfpropd  33993  elrspunidl  34034  elrspunsn  34035  mxidlmaxv  34049  mxidlirredi  34052  opprqusdrng  34073  qsdrnglem2  34076  dflringlem  34082  dflringlem2  34083  rprmcl  34106  rprmirred  34119  pidufd  34131  1arithufdlem3  34134  dfufd2  34138  zringfrac  34142  deg1prod  34171  ply1dg3rt0irred  34172  gsummoncoe1fzo  34185  mplvrpmrhm  34235  psrgsum  34236  psrmonprod  34240  esplyfval2  34253  lindsunlem  34312  fedgmullem1  34317  fedgmullem2  34318  assafld  34325  fldextrspunlsp  34362  extdgfialglem2  34381  irngnminplynz  34400  constrextdg2lem  34436  constrfiss  34439  constrsdrg  34463  submatminr1  34498  qtophaus  34524  qqhval2  34670  esummono  34742  gsumesum  34747  esum2dlem  34780  measvuni  34903  fiunelcarsg  35004  sitgclg  35030  sitgaddlemb  35036  eulerpartlemsv2  35046  eulerpartlemsv3  35049  eulerpartlemgc  35050  eulerpartlemv  35052  signstfvneq0  35257  signstfvcl  35258  signstfveq0a  35261  signstfveq0  35262  signsvfn  35267  signsvtp  35268  signsvtn  35269  signsvfpn  35270  signsvfnn  35271  signlem0  35272  hgt750leme  35343  onvf1odlem4  35991  iprodgam  36637  ttcwf2  37443  mh-inf3f1  37459  poimirlem2  38683  rrndstprj2  38908  lsatelbN  40206  lsatfixedN  40209  lkreqN  40370  lkrlspeqN  40371  dochnel2  42592  dochnel  42593  djhcvat42  42615  dochsnshp  42653  dochexmidat  42659  dochsnkr  42672  dochsnkr2  42673  dochsnkr2cl  42674  dochflcl  42675  dochfl1  42676  dochfln0  42677  lcfl6lem  42698  lcfl7lem  42699  lcfl8b  42704  lclkrlem2a  42707  lclkrlem2b  42708  lclkrlem2c  42709  lclkrlem2d  42710  lclkrlem2e  42711  lclkrlem2f  42712  lcfrlem14  42756  lcfrlem15  42757  lcfrlem16  42758  lcfrlem17  42759  lcfrlem18  42760  lcfrlem19  42761  lcfrlem20  42762  lcfrlem21  42763  lcfrlem23  42765  lcfrlem25  42767  lcfrlem26  42768  lcfrlem35  42777  lcfrlem36  42778  mapdn0  42869  mapdpglem29  42900  mapdpglem24  42904  baerlem3lem1  42907  baerlem5alem1  42908  baerlem5blem1  42909  baerlem3lem2  42910  baerlem5alem2  42911  baerlem5blem2  42912  baerlem5amN  42916  baerlem5bmN  42917  baerlem5abmN  42918  mapdindp0  42919  mapdindp1  42920  mapdindp2  42921  mapdindp3  42922  mapdindp4  42923  mapdheq2  42929  mapdheq4lem  42931  mapdheq4  42932  mapdh6lem1N  42933  mapdh6lem2N  42934  mapdh6aN  42935  mapdh6bN  42937  mapdh6cN  42938  mapdh6dN  42939  mapdh6eN  42940  mapdh6fN  42941  mapdh6gN  42942  mapdh6hN  42943  mapdh6iN  42944  mapdh7eN  42948  mapdh7cN  42949  mapdh7dN  42950  mapdh7fN  42951  mapdh75e  42952  mapdh75fN  42955  hvmaplfl  42967  mapdhvmap  42969  mapdh8aa  42976  mapdh8ab  42977  mapdh8ad  42979  mapdh8b  42980  mapdh8c  42981  mapdh8d0N  42982  mapdh8d  42983  mapdh8e  42984  mapdh9a  42989  mapdh9aOLDN  42990  hdmap1val2  43000  hdmap1eq  43001  hdmap1valc  43003  hdmap1eq2  43005  hdmap1eq4N  43006  hdmap1l6lem1  43007  hdmap1l6lem2  43008  hdmap1l6a  43009  hdmap1l6b  43011  hdmap1l6c  43012  hdmap1l6d  43013  hdmap1l6e  43014  hdmap1l6f  43015  hdmap1l6g  43016  hdmap1l6h  43017  hdmap1l6i  43018  hdmap1eulem  43022  hdmap1eulemOLDN  43023  hdmapcl  43030  hdmapval2lem  43031  hdmapval0  43033  hdmapeveclem  43034  hdmapevec  43035  hdmapval3lemN  43037  hdmapval3N  43038  hdmap10lem  43039  hdmap11lem1  43041  hdmap11lem2  43042  hdmapnzcl  43045  hdmaprnlem3N  43050  hdmaprnlem3uN  43051  hdmaprnlem4N  43053  hdmaprnlem7N  43055  hdmaprnlem8N  43056  hdmaprnlem9N  43057  hdmaprnlem3eN  43058  hdmaprnlem16N  43062  hdmap14lem1  43068  hdmap14lem2N  43069  hdmap14lem3  43070  hdmap14lem4a  43071  hdmap14lem6  43073  hdmap14lem8  43075  hdmap14lem9  43076  hdmap14lem10  43077  hdmap14lem11  43078  hdmap14lem12  43079  hgmaprnlem1N  43096  hgmaprnlem2N  43097  hgmaprnlem3N  43098  hgmaprnlem4N  43099  hdmapip1  43116  hdmapinvlem1  43118  hdmapinvlem2  43119  hdmapinvlem3  43120  hdmapinvlem4  43121  hdmapglem5  43122  hgmapvvlem1  43123  hgmapvvlem2  43124  hgmapvvlem3  43125  hdmapglem7a  43127  hdmapglem7b  43128  hdmapglem7  43129  evl1gprodd  43310  nelsubginvcld  43703  nelsubgcld  43704  nelsubgsubcld  43705  domnexpgn0cl  43727  fidomncyc  43742  frlmnzcoordex  43795  frlmnzcoordsca  43801  dffltz  43813  qirropth  44058  rmxyneg  44070  rmxm1  44084  rmxluc  44086  rmxdbl  44089  ltrmxnn0  44099  jm2.19lem1  44139  jm2.23  44146  rmxdiophlem  44165  aomclem2  44200  cantnftermord  44465  inaex  45424  bccm1k  45469  dstregt0  46440  fprodexp  46748  fprodabs2  46749  mccllem  46751  fprodcnlem  46753  climrec  46757  climdivf  46766  islpcn  46791  lptre2pt  46792  0ellimcdiv  46801  reclimc  46805  divlimc  46808  cncficcgt0  47040  dvdivf  47074  stoweidlem34  47186  stoweidlem43  47195  etransclem46  47432  etransclem47  47433  etransclem48  47434  hsphoidmvle2  47737  hsphoidmvle  47738  hoidmvlelem3  47749  hoidmvlelem4  47750  hspdifhsp  47768  readdcnnred  48515  resubcnnred  48516  recnmulnred  48517  cndivrenred  48518