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

Theorem eldifad 3780
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3778. (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 3778 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 210 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simpld 489 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 385  wcel 2157  cdif 3765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2776
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-v 3386  df-dif 3771
This theorem is referenced by:  xpdifid  5778  unblem1  8453  cantnflem3  8837  cantnflem4  8838  oef1o  8844  infxpenc  9126  acndom2  9162  ackbij1lem18  9346  infpssrlem3  9414  fin23lem26  9434  fin23lem30  9451  pwfseqlem4a  9770  expclz  13136  symgextf  18146  pmtrfinv  18190  symggen  18199  efgsdmi  18455  efgs1b  18459  efgsp1  18460  efgsres  18461  efgsresOLD  18462  efgredlemf  18465  efgredlemd  18468  efgredlem  18471  efgredlemOLD  18472  efgrelexlemb  18475  gsum2d2lem  18684  pgpfac1lem2  18787  pgpfac1lem3a  18788  pgpfac1lem3  18789  pgpfac1lem4  18790  isdrng2  19072  lvecinv  19431  lspsncmp  19434  lspsnne1  19435  lspsnnecom  19437  lspabs2  19438  lspsneu  19441  lspdisjb  19444  lspexch  19448  lspindp1  19452  lvecindp2  19458  lspsolv  19462  lspsnat  19464  lsppratlem1  19467  lsppratlem2  19468  fidomndrnglem  19626  frlmssuvc2  20456  maducoeval2  20769  hauscmplem  21535  1stccnp  21591  imasdsf1olem  22503  rrxmetlem  23526  divcncf  23552  dvrec  24056  dvmptdiv  24075  ftc1lem6  24142  elqaalem1  24412  elqaalem3  24414  ulmdvlem3  24494  abelthlem6  24528  abelthlem7a  24529  abelthlem7  24530  logtayl  24744  dmgmn0  25101  dmgmaddnn0  25102  dmgmdivn0  25103  lgamgulmlem2  25105  lgamgulmlem3  25106  lgamgulmlem5  25108  lgamgulmlem6  25109  lgamgulm2  25111  lgambdd  25112  lgamucov  25113  lgamcvg2  25130  gamcvg  25131  gamcvg2lem  25134  ftalem3  25150  lgsqrlem1  25420  lgsqrlem2  25421  lgsqrlem3  25422  lgsqrlem4  25423  lgseisenlem1  25449  lgseisenlem2  25450  lgseisenlem3  25451  lgseisenlem4  25452  lgseisen  25453  lgsquadlem2  25455  lgsquadlem3  25456  chebbnd1lem1  25507  dchrisum0re  25551  dchrisum0lema  25552  dchrisum0lem1b  25553  dchrisum0lem1  25554  dchrisum0lem2a  25555  dchrisum0lem2  25556  tgisline  25871  elntg  26214  uhgrss  26292  upgrex  26320  edguhgr  26357  1loopgrvd0  26747  disjiunel  29919  submatminr1  30385  qtophaus  30412  qqhval2  30535  esummono  30625  gsumesum  30630  esum2dlem  30663  measvuni  30786  fiunelcarsg  30887  sitgclg  30913  sitgaddlemb  30919  eulerpartlemsv2  30929  eulerpartlemsv3  30932  eulerpartlemgc  30933  eulerpartlemv  30935  signstfvneq0  31161  signstfvcl  31162  signstfveq0a  31165  signstfveq0  31166  signstfveq0OLD  31167  signsvfn  31172  signsvtp  31173  signsvtn  31174  signsvfpn  31175  signsvfnn  31176  signlem0  31177  hgt750leme  31249  iprodgam  32135  poimirlem2  33893  rrndstprj2  34110  lsatelbN  35020  lsatfixedN  35023  lkreqN  35184  lkrlspeqN  35185  dochnel2  37406  dochnel  37407  djhcvat42  37429  dochsnshp  37467  dochexmidat  37473  dochsnkr  37486  dochsnkr2  37487  dochsnkr2cl  37488  dochflcl  37489  dochfl1  37490  dochfln0  37491  lcfl6lem  37512  lcfl7lem  37513  lcfl8b  37518  lclkrlem2a  37521  lclkrlem2b  37522  lclkrlem2c  37523  lclkrlem2d  37524  lclkrlem2e  37525  lclkrlem2f  37526  lcfrlem14  37570  lcfrlem15  37571  lcfrlem16  37572  lcfrlem17  37573  lcfrlem18  37574  lcfrlem19  37575  lcfrlem20  37576  lcfrlem21  37577  lcfrlem23  37579  lcfrlem25  37581  lcfrlem26  37582  lcfrlem35  37591  lcfrlem36  37592  mapdn0  37683  mapdpglem29  37714  mapdpglem24  37718  baerlem3lem1  37721  baerlem5alem1  37722  baerlem5blem1  37723  baerlem3lem2  37724  baerlem5alem2  37725  baerlem5blem2  37726  baerlem5amN  37730  baerlem5bmN  37731  baerlem5abmN  37732  mapdindp0  37733  mapdindp1  37734  mapdindp2  37735  mapdindp3  37736  mapdindp4  37737  mapdheq2  37743  mapdheq4lem  37745  mapdheq4  37746  mapdh6lem1N  37747  mapdh6lem2N  37748  mapdh6aN  37749  mapdh6bN  37751  mapdh6cN  37752  mapdh6dN  37753  mapdh6eN  37754  mapdh6fN  37755  mapdh6gN  37756  mapdh6hN  37757  mapdh6iN  37758  mapdh7eN  37762  mapdh7cN  37763  mapdh7dN  37764  mapdh7fN  37765  mapdh75e  37766  mapdh75fN  37769  hvmaplfl  37781  mapdhvmap  37783  mapdh8aa  37790  mapdh8ab  37791  mapdh8ad  37793  mapdh8b  37794  mapdh8c  37795  mapdh8d0N  37796  mapdh8d  37797  mapdh8e  37798  mapdh9a  37803  mapdh9aOLDN  37804  hdmap1val2  37814  hdmap1eq  37815  hdmap1valc  37817  hdmap1eq2  37819  hdmap1eq4N  37820  hdmap1l6lem1  37821  hdmap1l6lem2  37822  hdmap1l6a  37823  hdmap1l6b  37825  hdmap1l6c  37826  hdmap1l6d  37827  hdmap1l6e  37828  hdmap1l6f  37829  hdmap1l6g  37830  hdmap1l6h  37831  hdmap1l6i  37832  hdmap1eulem  37836  hdmap1eulemOLDN  37837  hdmapcl  37844  hdmapval2lem  37845  hdmapval0  37847  hdmapeveclem  37848  hdmapevec  37849  hdmapval3lemN  37851  hdmapval3N  37852  hdmap10lem  37853  hdmap11lem1  37855  hdmap11lem2  37856  hdmapnzcl  37859  hdmaprnlem3N  37864  hdmaprnlem3uN  37865  hdmaprnlem4N  37867  hdmaprnlem7N  37869  hdmaprnlem8N  37870  hdmaprnlem9N  37871  hdmaprnlem3eN  37872  hdmaprnlem16N  37876  hdmap14lem1  37882  hdmap14lem2N  37883  hdmap14lem3  37884  hdmap14lem4a  37885  hdmap14lem6  37887  hdmap14lem8  37889  hdmap14lem9  37890  hdmap14lem10  37891  hdmap14lem11  37892  hdmap14lem12  37893  hgmaprnlem1N  37910  hgmaprnlem2N  37911  hgmaprnlem3N  37912  hgmaprnlem4N  37913  hdmapip1  37930  hdmapinvlem1  37932  hdmapinvlem2  37933  hdmapinvlem3  37934  hdmapinvlem4  37935  hdmapglem5  37936  hgmapvvlem1  37937  hgmapvvlem2  37938  hgmapvvlem3  37939  hdmapglem7a  37941  hdmapglem7b  37942  hdmapglem7  37943  qirropth  38247  rmxyneg  38259  rmxm1  38273  rmxluc  38275  rmxdbl  38278  ltrmxnn0  38290  jm2.19lem1  38330  jm2.23  38337  rmxdiophlem  38356  aomclem2  38399  bccm1k  39312  dstregt0  40228  fprodexp  40559  fprodabs2  40560  mccllem  40562  fprodcnlem  40564  climrec  40568  climdivf  40577  islpcn  40604  lptre2pt  40605  0ellimcdiv  40614  reclimc  40618  divlimc  40621  cncficcgt0  40834  dvdivf  40870  stoweidlem34  40983  stoweidlem43  40992  etransclem46  41229  etransclem47  41230  etransclem48  41231  hsphoidmvle2  41534  hsphoidmvle  41535  hoidmvlelem3  41546  hoidmvlelem4  41547  hspdifhsp  41565  zrzeroorngc  42790  zrtermoringc  42858  zrninitoringc  42859  nzerooringczr  42860
  Copyright terms: Public domain W3C validator