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

Theorem eldifad 3547
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3545. (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 3545 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 206 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simpld 473 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  wcel 1975  cdif 3532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-dif 3538
This theorem is referenced by:  xpdifid  5463  unblem1  8070  cantnflem3  8444  cantnflem4  8445  oef1o  8451  infxpenc  8697  acndom2  8733  ackbij1lem18  8915  infpssrlem3  8983  fin23lem26  9003  fin23lem30  9020  pwfseqlem4a  9335  expclz  12698  symgextf  17602  pmtrfinv  17646  symggen  17655  efgsdmi  17910  efgs1b  17914  efgsp1  17915  efgsres  17916  efgredlemf  17919  efgredlemd  17922  efgredlem  17925  efgrelexlemb  17928  gsum2d2lem  18137  pgpfac1lem2  18239  pgpfac1lem3a  18240  pgpfac1lem3  18241  pgpfac1lem4  18242  isdrng2  18522  lvecinv  18876  lspsncmp  18879  lspsnne1  18880  lspsnnecom  18882  lspabs2  18883  lspsneu  18886  lspdisjb  18889  lspexch  18892  lspindp1  18896  lvecindp2  18902  lspsolv  18906  lspsnat  18908  lsppratlem1  18910  lsppratlem2  18911  fidomndrnglem  19069  frlmssuvc2  19891  maducoeval2  20203  hauscmplem  20957  1stccnp  21013  imasdsf1olem  21925  rrxmetlem  22911  dvrec  23437  ftc1lem6  23521  elqaalem1  23791  elqaalem3  23793  ulmdvlem3  23873  abelthlem6  23907  abelthlem7a  23908  abelthlem7  23909  logtayl  24119  dmgmn0  24465  dmgmaddnn0  24466  dmgmdivn0  24467  lgamgulmlem2  24469  lgamgulmlem3  24470  lgamgulmlem5  24472  lgamgulmlem6  24473  lgamgulm2  24475  lgambdd  24476  lgamucov  24477  lgamcvg2  24494  gamcvg  24495  gamcvg2lem  24498  ftalem3  24514  lgsqrlem1  24784  lgsqrlem2  24785  lgsqrlem3  24786  lgsqrlem4  24787  lgseisenlem1  24813  lgseisenlem2  24814  lgseisenlem3  24815  lgseisenlem4  24816  lgseisen  24817  lgsquadlem2  24819  lgsquadlem3  24820  chebbnd1lem1  24871  dchrisum0re  24915  dchrisum0lema  24916  dchrisum0lem1b  24917  dchrisum0lem1  24918  dchrisum0lem2a  24919  dchrisum0lem2  24920  tgisline  25236  elntg  25578  uhgrass  25597  umgraex  25614  disjiunel  28593  submatminr1  29006  qtophaus  29033  qqhval2  29156  esummono  29245  gsumesum  29250  esum2dlem  29283  measvuni  29406  fiunelcarsg  29507  sitgclg  29533  sitgaddlemb  29539  eulerpartlemsv2  29549  eulerpartlemsv3  29552  eulerpartlemgc  29553  eulerpartlemv  29555  signstfvneq0  29777  signstfvcl  29778  signstfveq0a  29781  signstfveq0  29782  signsvfn  29787  signsvtp  29788  signsvtn  29789  signsvfpn  29790  signsvfnn  29791  signlem0  29792  iprodgam  30683  poimirlem2  32380  rrndstprj2  32599  lsatelbN  33110  lsatfixedN  33113  lkreqN  33274  lkrlspeqN  33275  dochnel2  35498  dochnel  35499  djhcvat42  35521  dochsnshp  35559  dochexmidat  35565  dochsnkr  35578  dochsnkr2  35579  dochsnkr2cl  35580  dochflcl  35581  dochfl1  35582  dochfln0  35583  lcfl6lem  35604  lcfl7lem  35605  lcfl8b  35610  lclkrlem2a  35613  lclkrlem2b  35614  lclkrlem2c  35615  lclkrlem2d  35616  lclkrlem2e  35617  lclkrlem2f  35618  lcfrlem14  35662  lcfrlem15  35663  lcfrlem16  35664  lcfrlem17  35665  lcfrlem18  35666  lcfrlem19  35667  lcfrlem20  35668  lcfrlem21  35669  lcfrlem23  35671  lcfrlem25  35673  lcfrlem26  35674  lcfrlem35  35683  lcfrlem36  35684  mapdn0  35775  mapdpglem29  35806  mapdpglem24  35810  baerlem3lem1  35813  baerlem5alem1  35814  baerlem5blem1  35815  baerlem3lem2  35816  baerlem5alem2  35817  baerlem5blem2  35818  baerlem5amN  35822  baerlem5bmN  35823  baerlem5abmN  35824  mapdindp0  35825  mapdindp1  35826  mapdindp2  35827  mapdindp3  35828  mapdindp4  35829  mapdheq2  35835  mapdheq4lem  35837  mapdheq4  35838  mapdh6lem1N  35839  mapdh6lem2N  35840  mapdh6aN  35841  mapdh6bN  35843  mapdh6cN  35844  mapdh6dN  35845  mapdh6eN  35846  mapdh6fN  35847  mapdh6gN  35848  mapdh6hN  35849  mapdh6iN  35850  mapdh7eN  35854  mapdh7cN  35855  mapdh7dN  35856  mapdh7fN  35857  mapdh75e  35858  mapdh75fN  35861  hvmaplfl  35873  mapdhvmap  35875  mapdh8aa  35882  mapdh8ab  35883  mapdh8ad  35885  mapdh8b  35886  mapdh8c  35887  mapdh8d0N  35888  mapdh8d  35889  mapdh8e  35890  mapdh9a  35896  mapdh9aOLDN  35897  hdmap1val2  35907  hdmap1eq  35908  hdmap1valc  35910  hdmap1eq2  35912  hdmap1eq4N  35913  hdmap1l6lem1  35914  hdmap1l6lem2  35915  hdmap1l6a  35916  hdmap1l6b  35918  hdmap1l6c  35919  hdmap1l6d  35920  hdmap1l6e  35921  hdmap1l6f  35922  hdmap1l6g  35923  hdmap1l6h  35924  hdmap1l6i  35925  hdmap1eulem  35930  hdmap1eulemOLDN  35931  hdmap1neglem1N  35934  hdmapcl  35939  hdmapval2lem  35940  hdmapval0  35942  hdmapeveclem  35943  hdmapevec  35944  hdmapval3lemN  35946  hdmapval3N  35947  hdmap10lem  35948  hdmap11lem1  35950  hdmap11lem2  35951  hdmapnzcl  35954  hdmaprnlem3N  35959  hdmaprnlem3uN  35960  hdmaprnlem4N  35962  hdmaprnlem7N  35964  hdmaprnlem8N  35965  hdmaprnlem9N  35966  hdmaprnlem3eN  35967  hdmaprnlem16N  35971  hdmap14lem1  35977  hdmap14lem2N  35978  hdmap14lem3  35979  hdmap14lem4a  35980  hdmap14lem6  35982  hdmap14lem8  35984  hdmap14lem9  35985  hdmap14lem10  35986  hdmap14lem11  35987  hdmap14lem12  35988  hgmaprnlem1N  36005  hgmaprnlem2N  36006  hgmaprnlem3N  36007  hgmaprnlem4N  36008  hdmapip1  36025  hdmapinvlem1  36027  hdmapinvlem2  36028  hdmapinvlem3  36029  hdmapinvlem4  36030  hdmapglem5  36031  hgmapvvlem1  36032  hgmapvvlem2  36033  hgmapvvlem3  36034  hdmapglem7a  36036  hdmapglem7b  36037  hdmapglem7  36038  qirropth  36290  rmxyneg  36302  rmxm1  36316  rmxluc  36318  rmxdbl  36321  ltrmxnn0  36333  jm2.19lem1  36373  jm2.23  36380  rmxdiophlem  36399  aomclem2  36442  bccm1k  37362  dstregt0  38233  fprodexp  38461  fprodabs2  38462  mccllem  38464  fprodcnlem  38466  climrec  38470  climdivf  38479  islpcn  38506  lptre2pt  38507  0ellimcdiv  38516  reclimc  38520  divlimc  38523  divcncf  38569  cncficcgt0  38574  dvmptdiv  38607  dvdivf  38612  stoweidlem34  38727  stoweidlem43  38736  etransclem46  38973  etransclem47  38974  etransclem48  38975  hsphoidmvle2  39275  hsphoidmvle  39276  hoidmvlelem3  39287  hoidmvlelem4  39288  hspdifhsp  39306  uhgrss  40284  upgrex  40316  edguhgr  40360  1loopgrvd0  40717  zrzeroorngc  41792  zrtermoringc  41860  zrninitoringc  41861  nzerooringczr  41862
  Copyright terms: Public domain W3C validator