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 493	1 ⊢ (𝜑 → 𝐴 ∈ 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3473  df-dif 3950

This theorem is referenced by:  xpdifid  6175  fvdifsupp  8180  unblem1  9324  cantnflem3  9720  cantnflem4  9721  oef1o  9727  infxpenc  10047  acndom2  10083  ackbij1lem18  10266  infpssrlem3  10334  fin23lem26  10354  fin23lem30  10371  pwfseqlem4a  10690  expclz  14087  symgextf  19377  pmtrfinv  19421  symggen  19430  efgsdmi  19692  efgs1b  19696  efgsp1  19697  efgsres  19698  efgredlemf  19701  efgredlemd  19704  efgredlemc  19705  efgredlem  19707  efgrelexlemb  19710  gsum2d2lem  19933  pgpfac1lem2  20037  pgpfac1lem3a  20038  pgpfac1lem3  20039  pgpfac1lem4  20040  zrzeroorngc  20582  zrtermoringc  20613  zrninitoringc  20614  isdrng2  20643  lvecinv  21006  lspsncmp  21009  lspsnne1  21010  lspsnnecom  21012  lspabs2  21013  lspsneu  21016  lspdisjb  21019  lspexch  21022  lspindp1  21026  lvecindp2  21032  lspsolv  21036  lspsnat  21038  lsppratlem1  21040  lsppratlem2  21041  fidomndrnglem  21265  nzerooringczr  21411  frlmssuvc2  21734  evls1fpws  22293  maducoeval2  22560  hauscmplem  23328  1stccnp  23384  imasdsf1olem  24297  rrxmetlem  25353  divcncf  25394  dvrec  25905  dvmptdiv  25924  ftc1lem6  25994  elqaalem1  26272  elqaalem3  26274  ulmdvlem3  26356  abelthlem6  26391  abelthlem7a  26392  abelthlem7  26393  logtayl  26612  dmgmn0  26976  dmgmaddnn0  26977  dmgmdivn0  26978  lgamgulmlem2  26980  lgamgulmlem3  26981  lgamgulmlem5  26983  lgamgulmlem6  26984  lgamgulm2  26986  lgambdd  26987  lgamucov  26988  lgamcvg2  27005  gamcvg  27006  gamcvg2lem  27009  ftalem3  27025  lgsqrlem1  27297  lgsqrlem2  27298  lgsqrlem3  27299  lgsqrlem4  27300  lgseisenlem1  27326  lgseisenlem2  27327  lgseisenlem3  27328  lgseisenlem4  27329  lgseisen  27330  lgsquadlem1  27331  lgsquadlem2  27332  lgsquadlem3  27333  chebbnd1lem1  27420  dchrisum0re  27464  dchrisum0lema  27465  dchrisum0lem1b  27466  dchrisum0lem1  27467  dchrisum0lem2a  27468  dchrisum0lem2  27469  tgisline  28449  elntg  28813  uhgrss  28895  upgrex  28923  edguhgr  28960  1loopgrvd0  29336  disjiunel  32404  suppovss  32483  nn0difffzod  32591  gsumhashmul  32788  odpmco  32827  pmtrcnel  32830  pmtrcnelor  32832  cycpmco2f1  32863  cycpmco2rn  32864  cycpmco2lem1  32865  cycpmco2lem2  32866  cycpmco2lem3  32867  cycpmco2lem4  32868  cycpmco2lem5  32869  cycpmco2lem6  32870  cycpmco2lem7  32871  cycpmco2  32872  cyc3co2  32879  tocyccntz  32883  cyc3conja  32896  idomrcan  32967  isdrng4  32980  fracfld  33012  zringfrac  33014  lindssn  33111  lindfpropd  33115  elrspunidl  33162  elrspunsn  33163  drngidl  33167  mxidlmaxv  33199  mxidlirredi  33202  opprqusdrng  33222  qsdrnglem2  33225  gsummoncoe1fzo  33273  lindsunlem  33327  fedgmullem1  33332  fedgmullem2  33333  irngnminplynz  33387  submatminr1  33416  qtophaus  33442  qqhval2  33588  esummono  33678  gsumesum  33683  esum2dlem  33716  measvuni  33838  fiunelcarsg  33941  sitgclg  33967  sitgaddlemb  33973  eulerpartlemsv2  33983  eulerpartlemsv3  33986  eulerpartlemgc  33987  eulerpartlemv  33989  signstfvneq0  34209  signstfvcl  34210  signstfveq0a  34213  signstfveq0  34214  signsvfn  34219  signsvtp  34220  signsvtn  34221  signsvfpn  34222  signsvfnn  34223  signlem0  34224  hgt750leme  34295  iprodgam  35341  poimirlem2  37100  rrndstprj2  37309  lsatelbN  38482  lsatfixedN  38485  lkreqN  38646  lkrlspeqN  38647  dochnel2  40869  dochnel  40870  djhcvat42  40892  dochsnshp  40930  dochexmidat  40936  dochsnkr  40949  dochsnkr2  40950  dochsnkr2cl  40951  dochflcl  40952  dochfl1  40953  dochfln0  40954  lcfl6lem  40975  lcfl7lem  40976  lcfl8b  40981  lclkrlem2a  40984  lclkrlem2b  40985  lclkrlem2c  40986  lclkrlem2d  40987  lclkrlem2e  40988  lclkrlem2f  40989  lcfrlem14  41033  lcfrlem15  41034  lcfrlem16  41035  lcfrlem17  41036  lcfrlem18  41037  lcfrlem19  41038  lcfrlem20  41039  lcfrlem21  41040  lcfrlem23  41042  lcfrlem25  41044  lcfrlem26  41045  lcfrlem35  41054  lcfrlem36  41055  mapdn0  41146  mapdpglem29  41177  mapdpglem24  41181  baerlem3lem1  41184  baerlem5alem1  41185  baerlem5blem1  41186  baerlem3lem2  41187  baerlem5alem2  41188  baerlem5blem2  41189  baerlem5amN  41193  baerlem5bmN  41194  baerlem5abmN  41195  mapdindp0  41196  mapdindp1  41197  mapdindp2  41198  mapdindp3  41199  mapdindp4  41200  mapdheq2  41206  mapdheq4lem  41208  mapdheq4  41209  mapdh6lem1N  41210  mapdh6lem2N  41211  mapdh6aN  41212  mapdh6bN  41214  mapdh6cN  41215  mapdh6dN  41216  mapdh6eN  41217  mapdh6fN  41218  mapdh6gN  41219  mapdh6hN  41220  mapdh6iN  41221  mapdh7eN  41225  mapdh7cN  41226  mapdh7dN  41227  mapdh7fN  41228  mapdh75e  41229  mapdh75fN  41232  hvmaplfl  41244  mapdhvmap  41246  mapdh8aa  41253  mapdh8ab  41254  mapdh8ad  41256  mapdh8b  41257  mapdh8c  41258  mapdh8d0N  41259  mapdh8d  41260  mapdh8e  41261  mapdh9a  41266  mapdh9aOLDN  41267  hdmap1val2  41277  hdmap1eq  41278  hdmap1valc  41280  hdmap1eq2  41282  hdmap1eq4N  41283  hdmap1l6lem1  41284  hdmap1l6lem2  41285  hdmap1l6a  41286  hdmap1l6b  41288  hdmap1l6c  41289  hdmap1l6d  41290  hdmap1l6e  41291  hdmap1l6f  41292  hdmap1l6g  41293  hdmap1l6h  41294  hdmap1l6i  41295  hdmap1eulem  41299  hdmap1eulemOLDN  41300  hdmapcl  41307  hdmapval2lem  41308  hdmapval0  41310  hdmapeveclem  41311  hdmapevec  41312  hdmapval3lemN  41314  hdmapval3N  41315  hdmap10lem  41316  hdmap11lem1  41318  hdmap11lem2  41319  hdmapnzcl  41322  hdmaprnlem3N  41327  hdmaprnlem3uN  41328  hdmaprnlem4N  41330  hdmaprnlem7N  41332  hdmaprnlem8N  41333  hdmaprnlem9N  41334  hdmaprnlem3eN  41335  hdmaprnlem16N  41339  hdmap14lem1  41345  hdmap14lem2N  41346  hdmap14lem3  41347  hdmap14lem4a  41348  hdmap14lem6  41350  hdmap14lem8  41352  hdmap14lem9  41353  hdmap14lem10  41354  hdmap14lem11  41355  hdmap14lem12  41356  hgmaprnlem1N  41373  hgmaprnlem2N  41374  hgmaprnlem3N  41375  hgmaprnlem4N  41376  hdmapip1  41393  hdmapinvlem1  41395  hdmapinvlem2  41396  hdmapinvlem3  41397  hdmapinvlem4  41398  hdmapglem5  41399  hgmapvvlem1  41400  hgmapvvlem2  41401  hgmapvvlem3  41402  hdmapglem7a  41404  hdmapglem7b  41405  hdmapglem7  41406  evl1gprodd  41592  nelsubginvcld  41739  nelsubgcld  41740  nelsubgsubcld  41741  prjspnfv01  42051  prjspner01  42052  prjspner1  42053  dffltz  42061  qirropth  42331  rmxyneg  42344  rmxm1  42358  rmxluc  42360  rmxdbl  42363  ltrmxnn0  42373  jm2.19lem1  42413  jm2.23  42420  rmxdiophlem  42439  aomclem2  42482  cantnftermord  42752  inaex  43737  bccm1k  43782  dstregt0  44665  fprodexp  44984  fprodabs2  44985  mccllem  44987  fprodcnlem  44989  climrec  44993  climdivf  45002  islpcn  45029  lptre2pt  45030  0ellimcdiv  45039  reclimc  45043  divlimc  45046  cncficcgt0  45278  dvdivf  45312  stoweidlem34  45424  stoweidlem43  45433  etransclem46  45670  etransclem47  45671  etransclem48  45672  hsphoidmvle2  45975  hsphoidmvle  45976  hoidmvlelem3  45987  hoidmvlelem4  45988  hspdifhsp  46006  readdcnnred  46685  resubcnnred  46686  recnmulnred  46687  cndivrenred  46688

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »