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

Theorem eldifad 3579
Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3577. (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 3577 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
31, 2sylib 208 . 2 (𝜑 → (𝐴𝐵 ∧ ¬ 𝐴𝐶))
43simpld 475 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wcel 1988  cdif 3564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570
This theorem is referenced by:  xpdifid  5550  unblem1  8197  cantnflem3  8573  cantnflem4  8574  oef1o  8580  infxpenc  8826  acndom2  8862  ackbij1lem18  9044  infpssrlem3  9112  fin23lem26  9132  fin23lem30  9149  pwfseqlem4a  9468  expclz  12868  symgextf  17818  pmtrfinv  17862  symggen  17871  efgsdmi  18126  efgs1b  18130  efgsp1  18131  efgsres  18132  efgredlemf  18135  efgredlemd  18138  efgredlem  18141  efgrelexlemb  18144  gsum2d2lem  18353  pgpfac1lem2  18455  pgpfac1lem3a  18456  pgpfac1lem3  18457  pgpfac1lem4  18458  isdrng2  18738  lvecinv  19094  lspsncmp  19097  lspsnne1  19098  lspsnnecom  19100  lspabs2  19101  lspsneu  19104  lspdisjb  19107  lspexch  19110  lspindp1  19114  lvecindp2  19120  lspsolv  19124  lspsnat  19126  lsppratlem1  19128  lsppratlem2  19129  fidomndrnglem  19287  frlmssuvc2  20115  maducoeval2  20427  hauscmplem  21190  1stccnp  21246  imasdsf1olem  22159  rrxmetlem  23171  divcncf  23197  dvrec  23699  dvmptdiv  23718  ftc1lem6  23785  elqaalem1  24055  elqaalem3  24057  ulmdvlem3  24137  abelthlem6  24171  abelthlem7a  24172  abelthlem7  24173  logtayl  24387  dmgmn0  24733  dmgmaddnn0  24734  dmgmdivn0  24735  lgamgulmlem2  24737  lgamgulmlem3  24738  lgamgulmlem5  24740  lgamgulmlem6  24741  lgamgulm2  24743  lgambdd  24744  lgamucov  24745  lgamcvg2  24762  gamcvg  24763  gamcvg2lem  24766  ftalem3  24782  lgsqrlem1  25052  lgsqrlem2  25053  lgsqrlem3  25054  lgsqrlem4  25055  lgseisenlem1  25081  lgseisenlem2  25082  lgseisenlem3  25083  lgseisenlem4  25084  lgseisen  25085  lgsquadlem2  25087  lgsquadlem3  25088  chebbnd1lem1  25139  dchrisum0re  25183  dchrisum0lema  25184  dchrisum0lem1b  25185  dchrisum0lem1  25186  dchrisum0lem2a  25187  dchrisum0lem2  25188  tgisline  25503  elntg  25845  uhgrss  25940  upgrex  25968  edguhgr  26005  1loopgrvd0  26381  disjiunel  29381  submatminr1  29850  qtophaus  29877  qqhval2  30000  esummono  30090  gsumesum  30095  esum2dlem  30128  measvuni  30251  fiunelcarsg  30352  sitgclg  30378  sitgaddlemb  30384  eulerpartlemsv2  30394  eulerpartlemsv3  30397  eulerpartlemgc  30398  eulerpartlemv  30400  signstfvneq0  30623  signstfvcl  30624  signstfveq0a  30627  signstfveq0  30628  signsvfn  30633  signsvtp  30634  signsvtn  30635  signsvfpn  30636  signsvfnn  30637  signlem0  30638  hgt750leme  30710  iprodgam  31603  poimirlem2  33382  rrndstprj2  33601  lsatelbN  34112  lsatfixedN  34115  lkreqN  34276  lkrlspeqN  34277  dochnel2  36500  dochnel  36501  djhcvat42  36523  dochsnshp  36561  dochexmidat  36567  dochsnkr  36580  dochsnkr2  36581  dochsnkr2cl  36582  dochflcl  36583  dochfl1  36584  dochfln0  36585  lcfl6lem  36606  lcfl7lem  36607  lcfl8b  36612  lclkrlem2a  36615  lclkrlem2b  36616  lclkrlem2c  36617  lclkrlem2d  36618  lclkrlem2e  36619  lclkrlem2f  36620  lcfrlem14  36664  lcfrlem15  36665  lcfrlem16  36666  lcfrlem17  36667  lcfrlem18  36668  lcfrlem19  36669  lcfrlem20  36670  lcfrlem21  36671  lcfrlem23  36673  lcfrlem25  36675  lcfrlem26  36676  lcfrlem35  36685  lcfrlem36  36686  mapdn0  36777  mapdpglem29  36808  mapdpglem24  36812  baerlem3lem1  36815  baerlem5alem1  36816  baerlem5blem1  36817  baerlem3lem2  36818  baerlem5alem2  36819  baerlem5blem2  36820  baerlem5amN  36824  baerlem5bmN  36825  baerlem5abmN  36826  mapdindp0  36827  mapdindp1  36828  mapdindp2  36829  mapdindp3  36830  mapdindp4  36831  mapdheq2  36837  mapdheq4lem  36839  mapdheq4  36840  mapdh6lem1N  36841  mapdh6lem2N  36842  mapdh6aN  36843  mapdh6bN  36845  mapdh6cN  36846  mapdh6dN  36847  mapdh6eN  36848  mapdh6fN  36849  mapdh6gN  36850  mapdh6hN  36851  mapdh6iN  36852  mapdh7eN  36856  mapdh7cN  36857  mapdh7dN  36858  mapdh7fN  36859  mapdh75e  36860  mapdh75fN  36863  hvmaplfl  36875  mapdhvmap  36877  mapdh8aa  36884  mapdh8ab  36885  mapdh8ad  36887  mapdh8b  36888  mapdh8c  36889  mapdh8d0N  36890  mapdh8d  36891  mapdh8e  36892  mapdh9a  36898  mapdh9aOLDN  36899  hdmap1val2  36909  hdmap1eq  36910  hdmap1valc  36912  hdmap1eq2  36914  hdmap1eq4N  36915  hdmap1l6lem1  36916  hdmap1l6lem2  36917  hdmap1l6a  36918  hdmap1l6b  36920  hdmap1l6c  36921  hdmap1l6d  36922  hdmap1l6e  36923  hdmap1l6f  36924  hdmap1l6g  36925  hdmap1l6h  36926  hdmap1l6i  36927  hdmap1eulem  36932  hdmap1eulemOLDN  36933  hdmap1neglem1N  36936  hdmapcl  36941  hdmapval2lem  36942  hdmapval0  36944  hdmapeveclem  36945  hdmapevec  36946  hdmapval3lemN  36948  hdmapval3N  36949  hdmap10lem  36950  hdmap11lem1  36952  hdmap11lem2  36953  hdmapnzcl  36956  hdmaprnlem3N  36961  hdmaprnlem3uN  36962  hdmaprnlem4N  36964  hdmaprnlem7N  36966  hdmaprnlem8N  36967  hdmaprnlem9N  36968  hdmaprnlem3eN  36969  hdmaprnlem16N  36973  hdmap14lem1  36979  hdmap14lem2N  36980  hdmap14lem3  36981  hdmap14lem4a  36982  hdmap14lem6  36984  hdmap14lem8  36986  hdmap14lem9  36987  hdmap14lem10  36988  hdmap14lem11  36989  hdmap14lem12  36990  hgmaprnlem1N  37007  hgmaprnlem2N  37008  hgmaprnlem3N  37009  hgmaprnlem4N  37010  hdmapip1  37027  hdmapinvlem1  37029  hdmapinvlem2  37030  hdmapinvlem3  37031  hdmapinvlem4  37032  hdmapglem5  37033  hgmapvvlem1  37034  hgmapvvlem2  37035  hgmapvvlem3  37036  hdmapglem7a  37038  hdmapglem7b  37039  hdmapglem7  37040  qirropth  37292  rmxyneg  37304  rmxm1  37318  rmxluc  37320  rmxdbl  37323  ltrmxnn0  37335  jm2.19lem1  37375  jm2.23  37382  rmxdiophlem  37401  aomclem2  37444  bccm1k  38361  dstregt0  39306  fprodexp  39626  fprodabs2  39627  mccllem  39629  fprodcnlem  39631  climrec  39635  climdivf  39644  islpcn  39671  lptre2pt  39672  0ellimcdiv  39681  reclimc  39685  divlimc  39688  cncficcgt0  39864  dvdivf  39900  stoweidlem34  40014  stoweidlem43  40023  etransclem46  40260  etransclem47  40261  etransclem48  40262  hsphoidmvle2  40562  hsphoidmvle  40563  hoidmvlelem3  40574  hoidmvlelem4  40575  hspdifhsp  40593  zrzeroorngc  41767  zrtermoringc  41835  zrninitoringc  41836  nzerooringczr  41837
  Copyright terms: Public domain W3C validator