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

Theorem eldifi 3311
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 3175 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 446 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1696    \ cdif 3162
This theorem is referenced by:  difss  3316  noel  3472  tz7.7  4434  tfi  4660  peano5  4695  tz7.48-1  6471  tz7.49  6473  dif20el  6520  oaf1o  6577  oeordi  6601  oeord  6602  oecan  6603  oeword  6604  oeworde  6607  oelimcl  6614  oeeulem  6615  oeeui  6616  oaabs2  6659  boxcutc  6875  domdifsn  6961  isinf  7092  pssnn  7097  unblem1  7125  pwfilem  7166  ordtypelem7  7255  unxpwdom2  7318  inf3lem3  7347  cantnfp1lem1  7396  cantnfp1lem3  7398  cantnflem3  7409  cantnflem4  7410  oef1o  7417  infxpenc  7661  infxpenc2lem1  7662  dfacacn  7783  infpssrlem3  7947  isf32lem3  7997  isf34lem4  8019  fin67  8037  isfin7-2  8038  domtriomlem  8084  axdc2lem  8090  axdc3lem4  8095  axdc4lem  8097  ttukeylem7  8158  konigthlem  8206  fpwwe2lem13  8280  fpwwe2  8281  pwfseqlem4a  8299  expclz  11144  hashf1lem1  11409  rlimrege0  12069  rlimrecl  12070  sumrblem  12200  fsumcvg  12201  summolem2a  12204  fsumss  12214  fsumless  12270  cvgcmpce  12292  binomlem  12303  incexclem  12311  incexc  12312  isumltss  12323  rpnnen2lem10  12518  rpnnen2lem11  12519  oddprm  12884  iserodd  12904  prmreclem2  12980  prmreclem3  12981  prmreclem5  12983  4sqlem19  13026  prmlem0  13123  firest  13353  grpinvnzcl  14556  sylow2alem2  14945  sylow2a  14946  efgsf  15054  efgsdmi  15057  efgsrel  15059  efgs1  15060  efgs1b  15061  efgsp1  15062  efgsres  15063  efgsfo  15064  efgredlemf  15066  efgredlemd  15069  efgredlemc  15070  efgredlem  15072  efgrelexlemb  15075  gsumzaddlem  15219  gsumzadd  15220  gsumzmhm  15226  gsumzinv  15233  gsumsub  15235  gsum2d2lem  15240  dprdfadd  15271  dprdsubg  15275  dprdres  15279  subgdmdprd  15285  dmdprdsplitlem  15288  dmdprdsplit2lem  15296  dpjidcl  15309  ablfac1b  15321  pgpfac1lem1  15325  pgpfac1lem2  15326  pgpfac1lem3a  15327  pgpfac1lem3  15328  pgpfac1lem4  15329  isirred  15497  irredrmul  15505  isdrng2  15538  isdrngd  15553  lbspropd  15868  lvecinv  15882  lspsncmp  15885  lspsnne1  15886  lspsnnecom  15888  lspabs2  15889  lspsneq  15891  lspsneu  15892  lspdisjb  15895  lspexch  15898  lspindp1  15902  lvecindp2  15908  lspsolv  15912  lspsnat  15914  lsppratlem6  15921  lbsextlem2  15928  lbsextlem4  15930  rngelnzr  16033  fidomndrnglem  16063  psrbaglesupp  16130  psrlidm  16164  psrridm  16165  mplsubglem  16195  mpllsslem  16196  mplsubrglem  16199  mplmonmul  16224  mplcoe1  16225  mplcoe2  16227  mplbas2  16228  coe1tmmul2  16368  coe1tmmul  16369  xrs1mnd  16425  xrs10  16426  xrs1cmn  16427  cnsubrg  16448  cmpfi  17151  2ndcdisj2  17199  1stccnp  17204  elptr2  17285  ptcnplem  17331  xkopt  17365  kqdisj  17439  fin1aufil  17643  ptcmplem2  17763  ptcmplem3  17764  ptcmplem4  17765  opnsubg  17806  lpbl  18065  blcld  18067  zcld  18335  recld2  18336  reconnlem1  18347  divcn  18388  iundisj  18921  mbfeqalem  19013  itg1val2  19055  itg1ge0  19057  i1fmullem  19065  i1fadd  19066  itg1addlem4  19070  itg1mulc  19075  itg1lea  19083  itg1le  19084  mbfi1fseqlem4  19089  itg2uba  19114  itg2lea  19115  itg2eqa  19116  itg2splitlem  19119  itg2split  19120  itgeqa  19184  ellimc3  19245  dvaddbr  19303  dvmulbr  19304  dvcobr  19311  dvcjbr  19314  dvrec  19320  dvcnvlem  19339  dvexp3  19341  dveflem  19342  ftc1lem6  19404  evlslem3  19414  tdeglem4  19462  mdeg0  19472  deg1n0ima  19491  deg1mul3le  19518  ig1peu  19573  ply1termlem  19601  plypf1  19610  plyaddlem1  19611  plymullem1  19612  coeeulem  19622  coeidlem  19635  coeid3  19638  coefv0  19645  coemulhi  19651  coemulc  19652  dvply1  19680  fta1  19704  vieta1lem2  19707  elaa  19712  elqaalem1  19715  elqaalem2  19716  aannenlem2  19725  aaliou2  19736  tayl0  19757  dvtaylp  19765  taylthlem1  19768  taylthlem2  19769  ulmdvlem3  19795  pserdvlem2  19820  abelthlem6  19828  abelthlem7a  19829  abelthlem7  19830  logtayl  20023  dcubic  20158  rlimcnp  20276  jensen  20299  wilthlem2  20323  basellem3  20336  chpub  20475  logexprlim  20480  lgslem1  20551  lgslem4  20554  lgsvalmod  20570  lgsqrlem1  20596  lgsqrlem2  20597  lgsqrlem3  20598  lgsqrlem4  20599  lgsqr  20601  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem3  20606  lgseisenlem4  20607  lgseisen  20608  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  lgsquad2  20615  m1lgs  20617  dchrisum0fno1  20676  dchrisum0re  20678  dchrisum0lema  20679  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  rplogsum  20692  ablomul  21038  mulid  21039  strlem1  22846  strlem3  22849  strlem4  22850  strlem5  22851  hstrlem3  22857  hstrlem4  22858  ballotlemi1  23077  ballotlemii  23078  ballotlemic  23081  ballotlem1c  23082  ballotlemscr  23093  ballotlemro  23097  ballotlemfg  23100  ballotlemfrc  23101  ballotlemfrceq  23103  ballotlemrinv0  23107  iundisjfi  23378  iundisjf  23380  logbcl  23414  measvuni  23557  ind0  23618  dmgmaddn0  23710  dmgmseqn0  23711  subfacp1lem1  23725  circum  24022  prodrblem  24152  fprodcvg  24153  prodmolem2a  24157  dfon2lem6  24215  wfrlem10  24336  wfrlem15  24341  itg2addnclem2  25004  ftc1cnnc  25025  dvreasin  25026  zerdivemp1  25539  bsstr  26231  nbssntr  26232  lppotos  26247  bsstrs  26249  nbssntrs  26250  bosser  26270  pdiveql  26271  neibastop1  26411  rrndstprj2  26658  isdrngo2  26692  isdrngo3  26693  divrngidl  26756  isfldidl  26796  pridlc2  26800  pridlc3  26801  prter2  26852  lcomfsup  26871  irrapx1  27016  pell1234qrne0  27041  pell1234qrreccl  27042  pell1234qrmulcl  27043  pell14qrgt0  27047  pell1234qrdich  27049  pell14qrdich  27057  pell1qrge1  27058  pell1qr1  27059  pell1qrgap  27062  pell14qrgapw  27064  pellqrexplicit  27065  pellqrex  27067  pellfundge  27070  pellfundgt1  27071  qirropth  27096  rmxyneg  27108  rmxm1  27122  rmxluc  27124  rmxdbl  27127  ltrmxnn0  27139  jm2.19lem1  27185  jm2.23  27192  rmxdiophlem  27211  setindtr  27220  aomclem2  27255  kelac1  27264  uvcresum  27345  frlmssuvc1  27349  frlmssuvc2  27350  frlmsslsp  27351  frlmup1  27353  frlmup2  27354  lindfrn  27394  f1lindf  27395  lindfmm  27400  islindf4  27411  mpaaeu  27458  flcidc  27482  pmtrf  27500  symggen  27514  mamulid  27561  mamurid  27562  cntzsdrg  27613  deg1mhm  27629  climrec  27832  stoweidlem25  27877  stoweidlem28  27880  stoweidlem34  27886  stoweidlem41  27893  stoweidlem43  27895  stoweidlem44  27896  stoweidlem46  27898  stirlinglem5  27930  uvtxnbgra  28306  elogb  28513  bnj923  29114  bnj570  29253  bnj594  29260  lsateln0  29807  lsatlss  29808  lsmsat  29820  lsatfixedN  29821  lsatcv0  29843  lsat0cv  29845  lcv1  29853  l1cvpat  29866  lkreqN  29982  lkrlspeqN  29983  dih1dimatlem  32141  dihatexv2  32151  dochnel2  32204  dochnel  32205  djhcvat42  32227  dihjat1lem  32240  dochsatshp  32263  dochsnshp  32265  dochexmidat  32271  dochsnkr  32284  dochsnkr2  32285  dochsnkr2cl  32286  dochflcl  32287  dochfl1  32288  dochfln0  32289  lcfl6lem  32310  lcfl7lem  32311  lcfl6  32312  lcfl8b  32316  lclkrlem2a  32319  lclkrlem2b  32320  lclkrlem2c  32321  lclkrlem2d  32322  lclkrlem2e  32323  lclkrlem2f  32324  lcfrlem14  32368  lcfrlem15  32369  lcfrlem16  32370  lcfrlem17  32371  lcfrlem18  32372  lcfrlem19  32373  lcfrlem20  32374  lcfrlem21  32375  lcfrlem23  32377  lcfrlem25  32379  lcfrlem26  32380  lcfrlem35  32389  lcfrlem36  32390  mapdrvallem2  32457  mapdn0  32481  mapdpglem29  32512  mapdpglem24  32516  mapdpglem32  32517  baerlem3lem1  32519  baerlem5alem1  32520  baerlem5blem1  32521  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  baerlem5amN  32528  baerlem5bmN  32529  baerlem5abmN  32530  mapdindp0  32531  mapdindp1  32532  mapdindp2  32533  mapdindp3  32534  mapdindp4  32535  mapdheq2  32541  mapdheq4lem  32543  mapdheq4  32544  mapdh6lem1N  32545  mapdh6lem2N  32546  mapdh6aN  32547  mapdh6bN  32549  mapdh6cN  32550  mapdh6dN  32551  mapdh6eN  32552  mapdh6fN  32553  mapdh6gN  32554  mapdh6hN  32555  mapdh6iN  32556  mapdh7eN  32560  mapdh7cN  32561  mapdh7dN  32562  mapdh7fN  32563  mapdh75e  32564  mapdh75fN  32567  hvmaplfl  32579  mapdhvmap  32581  mapdh8aa  32588  mapdh8ab  32589  mapdh8ad  32591  mapdh8b  32592  mapdh8c  32593  mapdh8d0N  32594  mapdh8d  32595  mapdh8e  32596  mapdh9a  32602  mapdh9aOLDN  32603  hdmap1val2  32613  hdmap1eq  32614  hdmap1valc  32616  hdmap1eq2  32618  hdmap1eq4N  32619  hdmap1l6lem1  32620  hdmap1l6lem2  32621  hdmap1l6a  32622  hdmap1l6b  32624  hdmap1l6c  32625  hdmap1l6d  32626  hdmap1l6e  32627  hdmap1l6f  32628  hdmap1l6g  32629  hdmap1l6h  32630  hdmap1l6i  32631  hdmap1eulem  32636  hdmap1eulemOLDN  32637  hdmap1neglem1N  32640  hdmapcl  32645  hdmapval2lem  32646  hdmapval0  32648  hdmapeveclem  32649  hdmapevec  32650  hdmapval3lemN  32652  hdmapval3N  32653  hdmap10lem  32654  hdmap11lem1  32656  hdmap11lem2  32657  hdmapnzcl  32660  hdmaprnlem3N  32665  hdmaprnlem3uN  32666  hdmaprnlem4N  32668  hdmaprnlem7N  32670  hdmaprnlem8N  32671  hdmaprnlem9N  32672  hdmaprnlem3eN  32673  hdmaprnlem16N  32677  hdmap14lem1  32683  hdmap14lem2N  32684  hdmap14lem3  32685  hdmap14lem4a  32686  hdmap14lem6  32688  hdmap14lem8  32690  hdmap14lem9  32691  hdmap14lem10  32692  hdmap14lem11  32693  hdmap14lem12  32694  hgmaprnlem1N  32711  hgmaprnlem2N  32712  hgmaprnlem3N  32713  hgmaprnlem4N  32714  hdmapip1  32731  hdmapinvlem1  32733  hdmapinvlem2  32734  hdmapinvlem3  32735  hdmapinvlem4  32736  hdmapglem5  32737  hgmapvvlem1  32738  hgmapvvlem2  32739  hgmapvvlem3  32740  hdmapglem7a  32742  hdmapglem7b  32743  hdmapglem7  32744
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168
  Copyright terms: Public domain W3C validator