MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldifi Unicode version

Theorem eldifi 3405
Description: Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldifi  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )

Proof of Theorem eldifi
StepHypRef Expression
1 eldif 3266 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 447 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1717    \ cdif 3253
This theorem is referenced by:  difss  3410  noel  3568  tz7.7  4541  tfi  4766  peano5  4801  tz7.48-1  6629  tz7.49  6631  dif20el  6678  oaf1o  6735  oeordi  6759  oeord  6760  oecan  6761  oeword  6762  oeworde  6765  oelimcl  6772  oeeulem  6773  oeeui  6774  oaabs2  6817  boxcutc  7034  domdifsn  7120  isinf  7251  pssnn  7256  pwfilem  7329  ordtypelem7  7419  unxpwdom2  7482  inf3lem3  7511  cantnfp1lem1  7560  cantnfp1lem3  7562  infxpenc2lem1  7826  dfacacn  7947  isf32lem3  8161  isf34lem4  8183  fin67  8201  isfin7-2  8202  domtriomlem  8248  axdc2lem  8254  axdc3lem4  8259  axdc4lem  8261  ttukeylem7  8321  konigthlem  8369  fpwwe2lem13  8443  fpwwe2  8444  hashf1lem1  11624  rlimrege0  12293  rlimrecl  12294  sumrblem  12425  fsumcvg  12426  summolem2a  12429  fsumss  12439  fsumless  12495  cvgcmpce  12517  binomlem  12528  incexclem  12536  incexc  12537  isumltss  12548  rpnnen2lem10  12743  rpnnen2lem11  12744  oddprm  13109  iserodd  13129  prmreclem2  13205  prmreclem3  13206  prmreclem5  13208  4sqlem19  13251  prmlem0  13348  firest  13580  grpinvnzcl  14783  sylow2alem2  15172  sylow2a  15173  efgsf  15281  efgsrel  15286  efgs1  15287  efgsfo  15291  efgredlemc  15297  gsumzaddlem  15446  gsumzadd  15447  gsumzmhm  15453  gsumzinv  15460  gsumsub  15462  gsum2d2lem  15467  dprdfadd  15498  dprdsubg  15502  dprdres  15506  subgdmdprd  15512  dmdprdsplitlem  15515  dmdprdsplit2lem  15523  dpjidcl  15536  ablfac1b  15548  pgpfac1lem1  15552  isirred  15724  irredrmul  15732  isdrng2  15765  isdrngd  15780  lbspropd  16091  lspsneq  16114  lsppratlem6  16144  lbsextlem2  16151  lbsextlem4  16153  rngelnzr  16256  psrbaglesupp  16353  psrlidm  16387  psrridm  16388  mplsubglem  16418  mpllsslem  16419  mplsubrglem  16422  mplmonmul  16447  mplcoe1  16448  mplcoe2  16450  mplbas2  16451  coe1tmmul2  16588  coe1tmmul  16589  xrs1mnd  16652  xrs10  16653  xrs1cmn  16654  cnsubrg  16675  cmpfi  17386  2ndcdisj2  17434  elptr2  17520  ptcnplem  17567  xkopt  17601  kqdisj  17678  fin1aufil  17878  ptcmplem2  17998  ptcmplem3  17999  ptcmplem4  18000  opnsubg  18051  lpbl  18416  blcld  18418  zcld  18708  recld2  18709  reconnlem1  18721  divcn  18762  iundisj  19302  mbfeqalem  19394  itg1val2  19436  itg1ge0  19438  i1fmullem  19446  i1fadd  19447  itg1addlem4  19451  itg1mulc  19456  itg1lea  19464  itg1le  19465  mbfi1fseqlem4  19470  itg2uba  19495  itg2lea  19496  itg2eqa  19497  itg2splitlem  19500  itg2split  19501  itgeqa  19565  ellimc3  19626  dvaddbr  19684  dvmulbr  19685  dvcobr  19692  dvcjbr  19695  dvrec  19701  dvcnvlem  19720  dvexp3  19722  dveflem  19723  evlslem3  19795  tdeglem4  19843  mdeg0  19853  deg1n0ima  19872  deg1mul3le  19899  ig1peu  19954  ply1termlem  19982  plypf1  19991  plyaddlem1  19992  plymullem1  19993  coeeulem  20003  coeidlem  20016  coeid3  20019  coefv0  20026  coemulhi  20032  coemulc  20033  dvply1  20061  fta1  20085  vieta1lem2  20088  elaa  20093  elqaalem2  20097  aannenlem2  20106  aaliou2  20117  tayl0  20138  dvtaylp  20146  taylthlem1  20149  taylthlem2  20150  pserdvlem2  20204  dcubic  20546  rlimcnp  20664  jensen  20687  wilthlem2  20712  basellem3  20725  chpub  20864  logexprlim  20869  lgslem1  20940  lgslem4  20943  lgsvalmod  20959  lgsqr  20990  lgsquadlem1  20998  lgsquad2  21004  m1lgs  21006  dchrisum0fno1  21065  rplogsum  21081  cusgraexi  21336  uvtxnbgra  21361  cusconngra  21504  ablomul  21784  mulid  21785  zerdivemp1  21863  strlem1  23594  strlem3  23597  strlem4  23598  strlem5  23599  hstrlem3  23605  hstrlem4  23606  iundisjf  23865  iundisjfi  23983  elzdif0  24156  logbcl  24186  ind0  24206  measvunilem  24353  ballotlem5  24529  ballotlemi1  24532  ballotlemii  24533  ballotlemic  24536  ballotlem1c  24537  ballotlemscr  24548  ballotlemro  24552  ballotlemfg  24555  ballotlemfrc  24556  ballotlemfrceq  24558  ballotlemrinv0  24562  dmgmaddn0  24579  dmlogdmgm  24580  lgamgulmlem2  24586  igamz  24604  gamp1  24614  regamcl  24617  subfacp1lem1  24637  circum  24883  prodrblem  25027  fprodcvg  25028  prodmolem2a  25032  fprodss  25046  dfon2lem6  25161  wfrlem10  25282  wfrlem15  25287  itg2addnclem2  25951  ftc1cnnc  25972  dvreasin  25973  neibastop1  26072  isdrngo2  26258  isdrngo3  26259  divrngidl  26322  isfldidl  26362  pridlc2  26366  pridlc3  26367  prter2  26414  lcomfsup  26431  irrapx1  26575  pell1234qrne0  26600  pell1234qrreccl  26601  pell1234qrmulcl  26602  pell14qrgt0  26606  pell1234qrdich  26608  pell14qrdich  26616  pell1qrge1  26617  pell1qr1  26618  pell1qrgap  26621  pell14qrgapw  26623  pellqrexplicit  26624  pellqrex  26626  pellfundge  26629  pellfundgt1  26630  setindtr  26779  kelac1  26823  uvcresum  26904  frlmssuvc1  26908  frlmsslsp  26910  frlmup1  26912  frlmup2  26913  lindfrn  26953  f1lindf  26954  lindfmm  26959  islindf4  26970  mpaaeu  27017  flcidc  27041  pmtrf  27059  mamulid  27120  mamurid  27121  cntzsdrg  27172  deg1mhm  27188  climrec  27390  stoweidlem25  27435  stoweidlem28  27438  stoweidlem41  27451  stoweidlem44  27454  stoweidlem46  27456  stirlinglem5  27488  frgrancvvdeqlem9  27786  frgrancvvdeq  27787  frgrancvvdgeq  27788  elogb  27871  bnj923  28468  bnj570  28607  bnj594  28614  lsateln0  29161  lsatlss  29162  lsmsat  29174  lsatcv0  29197  lsat0cv  29199  lcv1  29207  l1cvpat  29220  dih1dimatlem  31495  dihatexv2  31505  djhcvat42  31581  dihjat1lem  31594  dochsatshp  31617  lcfl6  31666  mapdrvallem2  31811  mapdpglem32  31871  mapdh9aOLDN  31957  hdmap1eulemOLDN  31991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-dif 3259
  Copyright terms: Public domain W3C validator