Theorem eldifad 3866

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3409  df-dif 3857

This theorem is referenced by:  xpdifid  5990  unblem1  8788  cantnflem3  9172  cantnflem4  9173  oef1o  9179  infxpenc  9463  acndom2  9499  ackbij1lem18  9682  infpssrlem3  9750  fin23lem26  9770  fin23lem30  9787  pwfseqlem4a  10106  expclz  13489  symgextf  18597  pmtrfinv  18641  symggen  18650  efgsdmi  18910  efgs1b  18914  efgsp1  18915  efgsres  18916  efgredlemf  18919  efgredlemd  18922  efgredlemc  18923  efgredlem  18925  efgrelexlemb  18928  gsum2d2lem  19146  pgpfac1lem2  19250  pgpfac1lem3a  19251  pgpfac1lem3  19252  pgpfac1lem4  19253  isdrng2  19565  lvecinv  19938  lspsncmp  19941  lspsnne1  19942  lspsnnecom  19944  lspabs2  19945  lspsneu  19948  lspdisjb  19951  lspexch  19954  lspindp1  19958  lvecindp2  19964  lspsolv  19968  lspsnat  19970  lsppratlem1  19972  lsppratlem2  19973  fidomndrnglem  20132  frlmssuvc2  20545  maducoeval2  21325  hauscmplem  22091  1stccnp  22147  imasdsf1olem  23060  rrxmetlem  24092  divcncf  24132  dvrec  24639  dvmptdiv  24658  ftc1lem6  24725  elqaalem1  24999  elqaalem3  25001  ulmdvlem3  25081  abelthlem6  25115  abelthlem7a  25116  abelthlem7  25117  logtayl  25335  dmgmn0  25695  dmgmaddnn0  25696  dmgmdivn0  25697  lgamgulmlem2  25699  lgamgulmlem3  25700  lgamgulmlem5  25702  lgamgulmlem6  25703  lgamgulm2  25705  lgambdd  25706  lgamucov  25707  lgamcvg2  25724  gamcvg  25725  gamcvg2lem  25728  ftalem3  25744  lgsqrlem1  26014  lgsqrlem2  26015  lgsqrlem3  26016  lgsqrlem4  26017  lgseisenlem1  26043  lgseisenlem2  26044  lgseisenlem3  26045  lgseisenlem4  26046  lgseisen  26047  lgsquadlem1  26048  lgsquadlem2  26049  lgsquadlem3  26050  chebbnd1lem1  26137  dchrisum0re  26181  dchrisum0lema  26182  dchrisum0lem1b  26183  dchrisum0lem1  26184  dchrisum0lem2a  26185  dchrisum0lem2  26186  tgisline  26505  elntg  26862  uhgrss  26941  upgrex  26969  edguhgr  27006  1loopgrvd0  27378  disjiunel  30442  suppovss  30526  fvdifsupp  30527  gsumhashmul  30827  odpmco  30866  pmtrcnel  30869  pmtrcnelor  30871  cycpmco2f1  30902  cycpmco2rn  30903  cycpmco2lem1  30904  cycpmco2lem2  30905  cycpmco2lem3  30906  cycpmco2lem4  30907  cycpmco2lem5  30908  cycpmco2lem6  30909  cycpmco2lem7  30910  cycpmco2  30911  cyc3co2  30918  tocyccntz  30922  cyc3conja  30935  lindssn  31079  lindfpropd  31082  elrspunidl  31112  lindsunlem  31211  fedgmullem1  31216  fedgmullem2  31217  submatminr1  31266  qtophaus  31292  qqhval2  31436  esummono  31526  gsumesum  31531  esum2dlem  31564  measvuni  31686  fiunelcarsg  31787  sitgclg  31813  sitgaddlemb  31819  eulerpartlemsv2  31829  eulerpartlemsv3  31832  eulerpartlemgc  31833  eulerpartlemv  31835  signstfvneq0  32055  signstfvcl  32056  signstfveq0a  32059  signstfveq0  32060  signsvfn  32065  signsvtp  32066  signsvtn  32067  signsvfpn  32068  signsvfnn  32069  signlem0  32070  hgt750leme  32142  iprodgam  33208  poimirlem2  35324  rrndstprj2  35534  lsatelbN  36567  lsatfixedN  36570  lkreqN  36731  lkrlspeqN  36732  dochnel2  38953  dochnel  38954  djhcvat42  38976  dochsnshp  39014  dochexmidat  39020  dochsnkr  39033  dochsnkr2  39034  dochsnkr2cl  39035  dochflcl  39036  dochfl1  39037  dochfln0  39038  lcfl6lem  39059  lcfl7lem  39060  lcfl8b  39065  lclkrlem2a  39068  lclkrlem2b  39069  lclkrlem2c  39070  lclkrlem2d  39071  lclkrlem2e  39072  lclkrlem2f  39073  lcfrlem14  39117  lcfrlem15  39118  lcfrlem16  39119  lcfrlem17  39120  lcfrlem18  39121  lcfrlem19  39122  lcfrlem20  39123  lcfrlem21  39124  lcfrlem23  39126  lcfrlem25  39128  lcfrlem26  39129  lcfrlem35  39138  lcfrlem36  39139  mapdn0  39230  mapdpglem29  39261  mapdpglem24  39265  baerlem3lem1  39268  baerlem5alem1  39269  baerlem5blem1  39270  baerlem3lem2  39271  baerlem5alem2  39272  baerlem5blem2  39273  baerlem5amN  39277  baerlem5bmN  39278  baerlem5abmN  39279  mapdindp0  39280  mapdindp1  39281  mapdindp2  39282  mapdindp3  39283  mapdindp4  39284  mapdheq2  39290  mapdheq4lem  39292  mapdheq4  39293  mapdh6lem1N  39294  mapdh6lem2N  39295  mapdh6aN  39296  mapdh6bN  39298  mapdh6cN  39299  mapdh6dN  39300  mapdh6eN  39301  mapdh6fN  39302  mapdh6gN  39303  mapdh6hN  39304  mapdh6iN  39305  mapdh7eN  39309  mapdh7cN  39310  mapdh7dN  39311  mapdh7fN  39312  mapdh75e  39313  mapdh75fN  39316  hvmaplfl  39328  mapdhvmap  39330  mapdh8aa  39337  mapdh8ab  39338  mapdh8ad  39340  mapdh8b  39341  mapdh8c  39342  mapdh8d0N  39343  mapdh8d  39344  mapdh8e  39345  mapdh9a  39350  mapdh9aOLDN  39351  hdmap1val2  39361  hdmap1eq  39362  hdmap1valc  39364  hdmap1eq2  39366  hdmap1eq4N  39367  hdmap1l6lem1  39368  hdmap1l6lem2  39369  hdmap1l6a  39370  hdmap1l6b  39372  hdmap1l6c  39373  hdmap1l6d  39374  hdmap1l6e  39375  hdmap1l6f  39376  hdmap1l6g  39377  hdmap1l6h  39378  hdmap1l6i  39379  hdmap1eulem  39383  hdmap1eulemOLDN  39384  hdmapcl  39391  hdmapval2lem  39392  hdmapval0  39394  hdmapeveclem  39395  hdmapevec  39396  hdmapval3lemN  39398  hdmapval3N  39399  hdmap10lem  39400  hdmap11lem1  39402  hdmap11lem2  39403  hdmapnzcl  39406  hdmaprnlem3N  39411  hdmaprnlem3uN  39412  hdmaprnlem4N  39414  hdmaprnlem7N  39416  hdmaprnlem8N  39417  hdmaprnlem9N  39418  hdmaprnlem3eN  39419  hdmaprnlem16N  39423  hdmap14lem1  39429  hdmap14lem2N  39430  hdmap14lem3  39431  hdmap14lem4a  39432  hdmap14lem6  39434  hdmap14lem8  39436  hdmap14lem9  39437  hdmap14lem10  39438  hdmap14lem11  39439  hdmap14lem12  39440  hgmaprnlem1N  39457  hgmaprnlem2N  39458  hgmaprnlem3N  39459  hgmaprnlem4N  39460  hdmapip1  39477  hdmapinvlem1  39479  hdmapinvlem2  39480  hdmapinvlem3  39481  hdmapinvlem4  39482  hdmapglem5  39483  hgmapvvlem1  39484  hgmapvvlem2  39485  hgmapvvlem3  39486  hdmapglem7a  39488  hdmapglem7b  39489  hdmapglem7  39490  nelsubginvcld  39712  nelsubgcld  39713  nelsubgsubcld  39714  prjspnfv01  39943  prjspner01  39944  prjspner1  39945  dffltz  39948  qirropth  40207  rmxyneg  40219  rmxm1  40233  rmxluc  40235  rmxdbl  40238  ltrmxnn0  40248  jm2.19lem1  40288  jm2.23  40295  rmxdiophlem  40314  aomclem2  40357  inaex  41363  bccm1k  41404  dstregt0  42265  fprodexp  42587  fprodabs2  42588  mccllem  42590  fprodcnlem  42592  climrec  42596  climdivf  42605  islpcn  42632  lptre2pt  42633  0ellimcdiv  42642  reclimc  42646  divlimc  42649  cncficcgt0  42881  dvdivf  42915  stoweidlem34  43027  stoweidlem43  43036  etransclem46  43273  etransclem47  43274  etransclem48  43275  hsphoidmvle2  43575  hsphoidmvle  43576  hoidmvlelem3  43587  hoidmvlelem4  43588  hspdifhsp  43606  readdcnnred  44213  resubcnnred  44214  recnmulnred  44215  cndivrenred  44216  zrzeroorngc  44978  zrtermoringc  45046  zrninitoringc  45047  nzerooringczr  45048