MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldifad Structured version   Visualization version   GIF version

Theorem eldifad 3727
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3725. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
eldifad.1 (𝜑𝐴 ∈ (𝐵𝐶))
Assertion
Ref Expression
eldifad (𝜑𝐴𝐵)

Proof of Theorem eldifad
StepHypRef Expression
1 eldifad.1 . . 3 (𝜑𝐴 ∈ (𝐵𝐶))
2 eldif 3725 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 208 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simpld 477 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  wcel 2139  cdif 3712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718
This theorem is referenced by:  xpdifid  5720  unblem1  8377  cantnflem3  8761  cantnflem4  8762  oef1o  8768  infxpenc  9031  acndom2  9067  ackbij1lem18  9251  infpssrlem3  9319  fin23lem26  9339  fin23lem30  9356  pwfseqlem4a  9675  expclz  13079  symgextf  18037  pmtrfinv  18081  symggen  18090  efgsdmi  18345  efgs1b  18349  efgsp1  18350  efgsres  18351  efgredlemf  18354  efgredlemd  18357  efgredlem  18360  efgrelexlemb  18363  gsum2d2lem  18572  pgpfac1lem2  18674  pgpfac1lem3a  18675  pgpfac1lem3  18676  pgpfac1lem4  18677  isdrng2  18959  lvecinv  19315  lspsncmp  19318  lspsnne1  19319  lspsnnecom  19321  lspabs2  19322  lspsneu  19325  lspdisjb  19328  lspexch  19331  lspindp1  19335  lvecindp2  19341  lspsolv  19345  lspsnat  19347  lsppratlem1  19349  lsppratlem2  19350  fidomndrnglem  19508  frlmssuvc2  20336  maducoeval2  20648  hauscmplem  21411  1stccnp  21467  imasdsf1olem  22379  rrxmetlem  23390  divcncf  23416  dvrec  23917  dvmptdiv  23936  ftc1lem6  24003  elqaalem1  24273  elqaalem3  24275  ulmdvlem3  24355  abelthlem6  24389  abelthlem7a  24390  abelthlem7  24391  logtayl  24605  dmgmn0  24951  dmgmaddnn0  24952  dmgmdivn0  24953  lgamgulmlem2  24955  lgamgulmlem3  24956  lgamgulmlem5  24958  lgamgulmlem6  24959  lgamgulm2  24961  lgambdd  24962  lgamucov  24963  lgamcvg2  24980  gamcvg  24981  gamcvg2lem  24984  ftalem3  25000  lgsqrlem1  25270  lgsqrlem2  25271  lgsqrlem3  25272  lgsqrlem4  25273  lgseisenlem1  25299  lgseisenlem2  25300  lgseisenlem3  25301  lgseisenlem4  25302  lgseisen  25303  lgsquadlem2  25305  lgsquadlem3  25306  chebbnd1lem1  25357  dchrisum0re  25401  dchrisum0lema  25402  dchrisum0lem1b  25403  dchrisum0lem1  25404  dchrisum0lem2a  25405  dchrisum0lem2  25406  tgisline  25721  elntg  26063  uhgrss  26158  upgrex  26186  edguhgr  26223  1loopgrvd0  26610  disjiunel  29716  submatminr1  30185  qtophaus  30212  qqhval2  30335  esummono  30425  gsumesum  30430  esum2dlem  30463  measvuni  30586  fiunelcarsg  30687  sitgclg  30713  sitgaddlemb  30719  eulerpartlemsv2  30729  eulerpartlemsv3  30732  eulerpartlemgc  30733  eulerpartlemv  30735  signstfvneq0  30958  signstfvcl  30959  signstfveq0a  30962  signstfveq0  30963  signsvfn  30968  signsvtp  30969  signsvtn  30970  signsvfpn  30971  signsvfnn  30972  signlem0  30973  hgt750leme  31045  iprodgam  31935  poimirlem2  33724  rrndstprj2  33943  lsatelbN  34796  lsatfixedN  34799  lkreqN  34960  lkrlspeqN  34961  dochnel2  37183  dochnel  37184  djhcvat42  37206  dochsnshp  37244  dochexmidat  37250  dochsnkr  37263  dochsnkr2  37264  dochsnkr2cl  37265  dochflcl  37266  dochfl1  37267  dochfln0  37268  lcfl6lem  37289  lcfl7lem  37290  lcfl8b  37295  lclkrlem2a  37298  lclkrlem2b  37299  lclkrlem2c  37300  lclkrlem2d  37301  lclkrlem2e  37302  lclkrlem2f  37303  lcfrlem14  37347  lcfrlem15  37348  lcfrlem16  37349  lcfrlem17  37350  lcfrlem18  37351  lcfrlem19  37352  lcfrlem20  37353  lcfrlem21  37354  lcfrlem23  37356  lcfrlem25  37358  lcfrlem26  37359  lcfrlem35  37368  lcfrlem36  37369  mapdn0  37460  mapdpglem29  37491  mapdpglem24  37495  baerlem3lem1  37498  baerlem5alem1  37499  baerlem5blem1  37500  baerlem3lem2  37501  baerlem5alem2  37502  baerlem5blem2  37503  baerlem5amN  37507  baerlem5bmN  37508  baerlem5abmN  37509  mapdindp0  37510  mapdindp1  37511  mapdindp2  37512  mapdindp3  37513  mapdindp4  37514  mapdheq2  37520  mapdheq4lem  37522  mapdheq4  37523  mapdh6lem1N  37524  mapdh6lem2N  37525  mapdh6aN  37526  mapdh6bN  37528  mapdh6cN  37529  mapdh6dN  37530  mapdh6eN  37531  mapdh6fN  37532  mapdh6gN  37533  mapdh6hN  37534  mapdh6iN  37535  mapdh7eN  37539  mapdh7cN  37540  mapdh7dN  37541  mapdh7fN  37542  mapdh75e  37543  mapdh75fN  37546  hvmaplfl  37558  mapdhvmap  37560  mapdh8aa  37567  mapdh8ab  37568  mapdh8ad  37570  mapdh8b  37571  mapdh8c  37572  mapdh8d0N  37573  mapdh8d  37574  mapdh8e  37575  mapdh9a  37581  mapdh9aOLDN  37582  hdmap1val2  37592  hdmap1eq  37593  hdmap1valc  37595  hdmap1eq2  37597  hdmap1eq4N  37598  hdmap1l6lem1  37599  hdmap1l6lem2  37600  hdmap1l6a  37601  hdmap1l6b  37603  hdmap1l6c  37604  hdmap1l6d  37605  hdmap1l6e  37606  hdmap1l6f  37607  hdmap1l6g  37608  hdmap1l6h  37609  hdmap1l6i  37610  hdmap1eulem  37615  hdmap1eulemOLDN  37616  hdmap1neglem1N  37619  hdmapcl  37624  hdmapval2lem  37625  hdmapval0  37627  hdmapeveclem  37628  hdmapevec  37629  hdmapval3lemN  37631  hdmapval3N  37632  hdmap10lem  37633  hdmap11lem1  37635  hdmap11lem2  37636  hdmapnzcl  37639  hdmaprnlem3N  37644  hdmaprnlem3uN  37645  hdmaprnlem4N  37647  hdmaprnlem7N  37649  hdmaprnlem8N  37650  hdmaprnlem9N  37651  hdmaprnlem3eN  37652  hdmaprnlem16N  37656  hdmap14lem1  37662  hdmap14lem2N  37663  hdmap14lem3  37664  hdmap14lem4a  37665  hdmap14lem6  37667  hdmap14lem8  37669  hdmap14lem9  37670  hdmap14lem10  37671  hdmap14lem11  37672  hdmap14lem12  37673  hgmaprnlem1N  37690  hgmaprnlem2N  37691  hgmaprnlem3N  37692  hgmaprnlem4N  37693  hdmapip1  37710  hdmapinvlem1  37712  hdmapinvlem2  37713  hdmapinvlem3  37714  hdmapinvlem4  37715  hdmapglem5  37716  hgmapvvlem1  37717  hgmapvvlem2  37718  hgmapvvlem3  37719  hdmapglem7a  37721  hdmapglem7b  37722  hdmapglem7  37723  qirropth  37975  rmxyneg  37987  rmxm1  38001  rmxluc  38003  rmxdbl  38006  ltrmxnn0  38018  jm2.19lem1  38058  jm2.23  38065  rmxdiophlem  38084  aomclem2  38127  bccm1k  39043  dstregt0  39992  fprodexp  40329  fprodabs2  40330  mccllem  40332  fprodcnlem  40334  climrec  40338  climdivf  40347  islpcn  40374  lptre2pt  40375  0ellimcdiv  40384  reclimc  40388  divlimc  40391  cncficcgt0  40604  dvdivf  40640  stoweidlem34  40754  stoweidlem43  40763  etransclem46  41000  etransclem47  41001  etransclem48  41002  hsphoidmvle2  41305  hsphoidmvle  41306  hoidmvlelem3  41317  hoidmvlelem4  41318  hspdifhsp  41336  zrzeroorngc  42512  zrtermoringc  42580  zrninitoringc  42581  nzerooringczr  42582
  Copyright terms: Public domain W3C validator