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

Theorem eldifad 3951
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3949. (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 3949 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 219 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simpld 495 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wcel 2107  cdif 3936
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-v 3501  df-dif 3942
This theorem is referenced by:  xpdifid  6022  unblem1  8762  cantnflem3  9146  cantnflem4  9147  oef1o  9153  infxpenc  9436  acndom2  9472  ackbij1lem18  9651  infpssrlem3  9719  fin23lem26  9739  fin23lem30  9756  pwfseqlem4a  10075  expclz  13447  symgextf  18467  pmtrfinv  18511  symggen  18520  efgsdmi  18780  efgs1b  18784  efgsp1  18785  efgsres  18786  efgredlemf  18789  efgredlemd  18792  efgredlemc  18793  efgredlem  18795  efgrelexlemb  18798  gsum2d2lem  19015  pgpfac1lem2  19119  pgpfac1lem3a  19120  pgpfac1lem3  19121  pgpfac1lem4  19122  isdrng2  19434  lvecinv  19807  lspsncmp  19810  lspsnne1  19811  lspsnnecom  19813  lspabs2  19814  lspsneu  19817  lspdisjb  19820  lspexch  19823  lspindp1  19827  lvecindp2  19833  lspsolv  19837  lspsnat  19839  lsppratlem1  19841  lsppratlem2  19842  fidomndrnglem  20000  frlmssuvc2  20857  maducoeval2  21167  hauscmplem  21932  1stccnp  21988  imasdsf1olem  22900  rrxmetlem  23927  divcncf  23965  dvrec  24469  dvmptdiv  24488  ftc1lem6  24555  elqaalem1  24825  elqaalem3  24827  ulmdvlem3  24907  abelthlem6  24941  abelthlem7a  24942  abelthlem7  24943  logtayl  25158  dmgmn0  25519  dmgmaddnn0  25520  dmgmdivn0  25521  lgamgulmlem2  25523  lgamgulmlem3  25524  lgamgulmlem5  25526  lgamgulmlem6  25527  lgamgulm2  25529  lgambdd  25530  lgamucov  25531  lgamcvg2  25548  gamcvg  25549  gamcvg2lem  25552  ftalem3  25568  lgsqrlem1  25838  lgsqrlem2  25839  lgsqrlem3  25840  lgsqrlem4  25841  lgseisenlem1  25867  lgseisenlem2  25868  lgseisenlem3  25869  lgseisenlem4  25870  lgseisen  25871  lgsquadlem1  25872  lgsquadlem2  25873  lgsquadlem3  25874  chebbnd1lem1  25961  dchrisum0re  26005  dchrisum0lema  26006  dchrisum0lem1b  26007  dchrisum0lem1  26008  dchrisum0lem2a  26009  dchrisum0lem2  26010  tgisline  26329  elntg  26686  uhgrss  26765  upgrex  26793  edguhgr  26830  1loopgrvd0  27202  disjiunel  30263  suppovss  30343  odpmco  30646  pmtrcnel  30649  pmtrcnelor  30651  cycpmco2f1  30682  cycpmco2rn  30683  cycpmco2lem1  30684  cycpmco2lem2  30685  cycpmco2lem3  30686  cycpmco2lem4  30687  cycpmco2lem5  30688  cycpmco2lem6  30689  cycpmco2lem7  30690  cycpmco2  30691  cyc3co2  30698  tocyccntz  30702  cyc3conja  30715  lindssn  30855  lindfpropd  30858  lindsunlem  30908  fedgmullem1  30913  fedgmullem2  30914  submatminr1  30963  qtophaus  30988  qqhval2  31111  esummono  31201  gsumesum  31206  esum2dlem  31239  measvuni  31361  fiunelcarsg  31462  sitgclg  31488  sitgaddlemb  31494  eulerpartlemsv2  31504  eulerpartlemsv3  31507  eulerpartlemgc  31508  eulerpartlemv  31510  signstfvneq0  31730  signstfvcl  31731  signstfveq0a  31734  signstfveq0  31735  signsvfn  31740  signsvtp  31741  signsvtn  31742  signsvfpn  31743  signsvfnn  31744  signlem0  31745  hgt750leme  31817  iprodgam  32860  poimirlem2  34763  rrndstprj2  34979  lsatelbN  36011  lsatfixedN  36014  lkreqN  36175  lkrlspeqN  36176  dochnel2  38397  dochnel  38398  djhcvat42  38420  dochsnshp  38458  dochexmidat  38464  dochsnkr  38477  dochsnkr2  38478  dochsnkr2cl  38479  dochflcl  38480  dochfl1  38481  dochfln0  38482  lcfl6lem  38503  lcfl7lem  38504  lcfl8b  38509  lclkrlem2a  38512  lclkrlem2b  38513  lclkrlem2c  38514  lclkrlem2d  38515  lclkrlem2e  38516  lclkrlem2f  38517  lcfrlem14  38561  lcfrlem15  38562  lcfrlem16  38563  lcfrlem17  38564  lcfrlem18  38565  lcfrlem19  38566  lcfrlem20  38567  lcfrlem21  38568  lcfrlem23  38570  lcfrlem25  38572  lcfrlem26  38573  lcfrlem35  38582  lcfrlem36  38583  mapdn0  38674  mapdpglem29  38705  mapdpglem24  38709  baerlem3lem1  38712  baerlem5alem1  38713  baerlem5blem1  38714  baerlem3lem2  38715  baerlem5alem2  38716  baerlem5blem2  38717  baerlem5amN  38721  baerlem5bmN  38722  baerlem5abmN  38723  mapdindp0  38724  mapdindp1  38725  mapdindp2  38726  mapdindp3  38727  mapdindp4  38728  mapdheq2  38734  mapdheq4lem  38736  mapdheq4  38737  mapdh6lem1N  38738  mapdh6lem2N  38739  mapdh6aN  38740  mapdh6bN  38742  mapdh6cN  38743  mapdh6dN  38744  mapdh6eN  38745  mapdh6fN  38746  mapdh6gN  38747  mapdh6hN  38748  mapdh6iN  38749  mapdh7eN  38753  mapdh7cN  38754  mapdh7dN  38755  mapdh7fN  38756  mapdh75e  38757  mapdh75fN  38760  hvmaplfl  38772  mapdhvmap  38774  mapdh8aa  38781  mapdh8ab  38782  mapdh8ad  38784  mapdh8b  38785  mapdh8c  38786  mapdh8d0N  38787  mapdh8d  38788  mapdh8e  38789  mapdh9a  38794  mapdh9aOLDN  38795  hdmap1val2  38805  hdmap1eq  38806  hdmap1valc  38808  hdmap1eq2  38810  hdmap1eq4N  38811  hdmap1l6lem1  38812  hdmap1l6lem2  38813  hdmap1l6a  38814  hdmap1l6b  38816  hdmap1l6c  38817  hdmap1l6d  38818  hdmap1l6e  38819  hdmap1l6f  38820  hdmap1l6g  38821  hdmap1l6h  38822  hdmap1l6i  38823  hdmap1eulem  38827  hdmap1eulemOLDN  38828  hdmapcl  38835  hdmapval2lem  38836  hdmapval0  38838  hdmapeveclem  38839  hdmapevec  38840  hdmapval3lemN  38842  hdmapval3N  38843  hdmap10lem  38844  hdmap11lem1  38846  hdmap11lem2  38847  hdmapnzcl  38850  hdmaprnlem3N  38855  hdmaprnlem3uN  38856  hdmaprnlem4N  38858  hdmaprnlem7N  38860  hdmaprnlem8N  38861  hdmaprnlem9N  38862  hdmaprnlem3eN  38863  hdmaprnlem16N  38867  hdmap14lem1  38873  hdmap14lem2N  38874  hdmap14lem3  38875  hdmap14lem4a  38876  hdmap14lem6  38878  hdmap14lem8  38880  hdmap14lem9  38881  hdmap14lem10  38882  hdmap14lem11  38883  hdmap14lem12  38884  hgmaprnlem1N  38901  hgmaprnlem2N  38902  hgmaprnlem3N  38903  hgmaprnlem4N  38904  hdmapip1  38921  hdmapinvlem1  38923  hdmapinvlem2  38924  hdmapinvlem3  38925  hdmapinvlem4  38926  hdmapglem5  38927  hgmapvvlem1  38928  hgmapvvlem2  38929  hgmapvvlem3  38930  hdmapglem7a  38932  hdmapglem7b  38933  hdmapglem7  38934  nelsubginvcld  38995  nelsubgcld  38996  nelsubgsubcld  38997  dffltz  39138  qirropth  39372  rmxyneg  39384  rmxm1  39398  rmxluc  39400  rmxdbl  39403  ltrmxnn0  39413  jm2.19lem1  39453  jm2.23  39460  rmxdiophlem  39479  aomclem2  39522  inaex  40500  bccm1k  40541  dstregt0  41414  fprodexp  41742  fprodabs2  41743  mccllem  41745  fprodcnlem  41747  climrec  41751  climdivf  41760  islpcn  41787  lptre2pt  41788  0ellimcdiv  41797  reclimc  41801  divlimc  41804  cncficcgt0  42038  dvdivf  42074  stoweidlem34  42187  stoweidlem43  42196  etransclem46  42433  etransclem47  42434  etransclem48  42435  hsphoidmvle2  42735  hsphoidmvle  42736  hoidmvlelem3  42747  hoidmvlelem4  42748  hspdifhsp  42766  readdcnnred  43371  resubcnnred  43372  recnmulnred  43373  cndivrenred  43374  zrzeroorngc  44107  zrtermoringc  44175  zrninitoringc  44176  nzerooringczr  44177
  Copyright terms: Public domain W3C validator