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

Theorem eldifi 3612
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 3471 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 458 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1823    \ cdif 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-dif 3464
This theorem is referenced by:  difss  3617  noel  3787  tz7.7  4893  xpdifid  5420  tfi  6661  peano5  6696  tz7.48-1  7100  tz7.49  7102  dif20el  7147  oaf1o  7204  oeordi  7228  oeord  7229  oecan  7230  oeword  7231  oeworde  7234  oelimcl  7241  oeeulem  7242  oeeui  7243  oaabs2  7286  boxcutc  7505  domdifsn  7593  isinf  7726  pssnn  7731  pwfilem  7806  fsuppco2  7854  fsuppcor  7855  ordtypelem7  7941  unxpwdom2  8006  inf3lem3  8038  cantnfp1lem1  8088  cantnfp1lem3  8090  cantnfp1lem1OLD  8114  cantnfp1lem3OLD  8116  infxpenc2lem1  8387  dfacacn  8512  isf32lem3  8726  isf34lem4  8748  fin67  8766  isfin7-2  8767  domtriomlem  8813  axdc2lem  8819  axdc3lem4  8824  axdc4lem  8826  ttukeylem7  8886  konigthlem  8934  fpwwe2lem13  9009  fpwwe2  9010  hashf1lem1  12488  rlimrege0  13484  rlimrecl  13485  sumrblem  13615  fsumcvg  13616  summolem2a  13619  fsumss  13629  fsumless  13692  cvgcmpce  13714  binomlem  13723  incexclem  13730  incexc  13731  isumltss  13742  prodrblem  13818  fprodcvg  13819  prodmolem2a  13823  fprodss  13837  rpnnen2lem10  14041  rpnnen2lem11  14042  oddprm  14423  iserodd  14443  prmreclem2  14519  prmreclem3  14520  prmreclem5  14522  4sqlem19  14565  prmlem0  14675  firest  14922  grpinvnzcl  16309  symgextfv  16642  pmtrf  16679  pmtrdifellem3  16702  sylow2alem2  16837  sylow2a  16838  efgsf  16946  efgsrel  16951  efgs1  16952  efgsfo  16956  efgredlemc  16962  gsumzaddlem  17133  gsumzadd  17134  gsumzaddlemOLD  17135  gsumzaddOLD  17136  gsumzmhm  17155  gsumzmhmOLD  17156  gsumzinvOLD  17168  gsum2d2lem  17197  dprdfadd  17255  dprdfaddOLD  17262  dprdres  17270  subgdmdprd  17276  dmdprdsplitlem  17279  dmdprdsplitlemOLD  17280  dmdprdsplit2lem  17289  dpjidcl  17302  dpjidclOLD  17309  ablfac1b  17316  pgpfac1lem1  17320  gsummgp0  17451  isirred  17543  irredrmul  17551  isdrng2  17601  isdrngd  17616  lcomfsupOLD  17744  lcomfsupp  17745  lbspropd  17940  lspsneq  17963  lsppratlem6  17993  lbsextlem2  18000  lbsextlem4  18002  ringelnzr  18109  psrbaglesupp  18212  psrbaglesuppOLD  18213  psrlidm  18251  psrlidmOLD  18252  psrridm  18253  psrridmOLD  18254  mplsubglem  18288  mpllsslem  18289  mplsubglemOLD  18290  mpllsslemOLD  18291  mplsubrglem  18295  mplsubrglemOLD  18296  mplmonmul  18321  mplcoe1  18322  mplcoe5  18326  mplcoe2OLD  18328  mplbas2  18329  mplbas2OLD  18330  evlslem3  18378  coe1tmmul2  18512  coe1tmmul  18513  xrs1mnd  18651  xrs10  18652  xrs1cmn  18653  cnsubrg  18673  psgnodpm  18797  zrhpsgnodpm  18801  evpmodpmf1o  18805  uvcresum  18995  frlmssuvc1  18996  frlmsslsp  18998  frlmup2  19001  lindfrn  19023  f1lindf  19024  lindfmm  19029  islindf4  19040  dmatmul  19166  1marepvsma1  19252  mdetdiaglem  19267  mdetrlin  19271  mdetrsca  19272  mdetralt  19277  maducoeval2  19309  madugsum  19312  symgmatr01  19323  gsummatr01lem3  19326  gsummatr01lem4  19327  gsummatr01  19328  smadiadetlem0  19330  smadiadetlem1a  19332  cmpfi  20075  2ndcdisj2  20124  elptr2  20241  ptcnplem  20288  xkopt  20322  kqdisj  20399  fin1aufil  20599  ptcmplem2  20719  ptcmplem3  20720  ptcmplem4  20721  opnsubg  20772  lpbl  21172  blcld  21174  zcld  21484  recld2  21485  reconnlem1  21497  divcn  21538  iundisj  22124  mbfeqalem  22215  itg1val2  22257  itg1ge0  22259  i1fmullem  22267  i1fadd  22268  itg1addlem4  22272  itg1mulc  22277  itg1lea  22285  itg1le  22286  mbfi1fseqlem4  22291  itg2uba  22316  itg2lea  22317  itg2eqa  22318  itg2splitlem  22321  itg2split  22322  itgeqa  22386  ellimc3  22449  dvaddbr  22507  dvmulbr  22508  dvcobr  22515  dvcjbr  22518  dvrec  22524  dvcnvlem  22543  dvexp3  22545  dveflem  22546  tdeglem4  22624  deg1n0ima  22655  deg1mul3le  22683  ig1peu  22738  ply1termlem  22766  plypf1  22775  plyaddlem1  22776  plymullem1  22777  coeeulem  22787  coeidlem  22800  coeid3  22803  coefv0  22811  coemulhi  22817  coemulc  22818  dvply1  22846  fta1  22870  vieta1lem2  22873  elaa  22878  elqaalem2  22882  aannenlem2  22891  aaliou2  22902  tayl0  22923  dvtaylp  22931  taylthlem1  22934  taylthlem2  22935  pserdvlem2  22989  logbcl  23306  relogbreexp  23314  relogbcxp  23324  cxplogb  23325  dcubic  23374  rlimcnp  23493  jensen  23516  wilthlem2  23541  basellem3  23554  chpub  23693  logexprlim  23698  lgslem1  23769  lgslem4  23772  lgsvalmod  23788  lgsqr  23819  lgsquadlem1  23827  lgsquad2  23833  m1lgs  23835  dchrisum0fno1  23894  rplogsum  23910  ishpg  24329  cusgraexi  24670  uvtxnbgra  24695  cusconngra  24878  frgrancvvdeqlem9  25243  frgrancvvdeq  25244  frgrancvvdgeq  25245  2spotiundisj  25264  frghash2spot  25265  ablomul  25555  mulid  25556  zerdivemp1  25634  strlem1  27367  strlem3  27370  strlem4  27371  strlem5  27372  hstrlem3  27378  hstrlem4  27379  iundisjf  27659  suppss3  27781  iundisjfi  27835  qtophaus  28074  elzdif0  28195  ind0  28249  measvunilem  28420  sibfof  28546  eulerpartlemb  28571  eulerpartlemf  28573  sseqf  28595  ballotlem5  28702  ballotlemi1  28705  ballotlemii  28706  ballotlemic  28709  ballotlem1c  28710  ballotlemscr  28721  ballotlemro  28725  ballotlemfg  28728  ballotlemfrc  28729  ballotlemfrceq  28731  ballotlemrinv0  28735  plymulx0  28768  signstfvn  28790  dmgmaddn0  28829  dmlogdmgm  28830  lgamgulmlem2  28836  igamz  28854  gamp1  28864  regamcl  28867  subfacp1lem1  28887  mrsubcn  29143  mrsubco  29145  circum  29304  dfon2lem6  29460  wfrlem10  29592  wfrlem15  29597  dvtan  30305  itg2addnclem2  30307  ftc1cnnc  30329  dvasin  30343  dvreasin  30345  dvreacos  30346  neibastop1  30417  isdrngo2  30601  isdrngo3  30602  divrngidl  30665  isfldidl  30705  pridlc2  30709  pridlc3  30710  prter2  30862  irrapx1  31003  pell1234qrne0  31028  pell1234qrreccl  31029  pell1234qrmulcl  31030  pell14qrgt0  31034  pell1234qrdich  31036  pell14qrdich  31044  pell1qrge1  31045  pell1qr1  31046  pell1qrgap  31049  pell14qrgapw  31051  pellqrexplicit  31052  pellqrex  31054  pellfundge  31057  pellfundgt1  31058  setindtr  31205  kelac1  31248  mpaaeu  31340  flcidc  31364  cntzsdrg  31392  deg1mhm  31408  radcnvrat  31436  binomcxplemdvbinom  31499  icoiccdif  31803  fsumnncl  31811  fsumsplit1  31812  fprodn0f  31833  fprodeq0g  31840  fprod0  31842  climrec  31848  islpcn  31884  lptre2pt  31885  limclner  31896  fprodcncf  31943  dvrecg  31946  fperdvper  31954  dvdivcncf  31963  dvnmul  31979  dvmptfprodlem  31980  dvnprodlem2  31983  stoweidlem25  32046  stoweidlem28  32049  stoweidlem41  32062  stoweidlem44  32065  stoweidlem46  32067  stirlinglem5  32099  dirkercncflem1  32124  dirkercncflem2  32125  fourierdlem24  32152  fourierdlem62  32190  fouriersw  32253  fouriercn  32254  elaa2lem  32255  elaa2  32256  etransclem25  32281  etransclem35  32291  etransclem44  32300  fsummsndifre  32717  fsummmodsndifre  32719  c0rhm  32972  c0rnghm  32973  zrrnghm  32977  2zrngnmlid2  33011  zrinitorngc  33062  zrtermorngc  33063  mgpsumunsn  33205  mgpsumz  33206  mgpsumn  33207  lindslinindsimp1  33312  lindslinindsimp2  33318  lincresunit1  33332  lincresunit2  33333  lincresunit3lem1  33334  lincresunit3lem2  33335  lincresunit3  33336  lindssnlvec  33341  logcxp0  33410  relogbmulbexp  33436  relogbdivb  33437  dignn0fr  33476  bnj923  34227  bnj570  34364  bnj594  34371  lsateln0  35117  lsatlss  35118  lsmsat  35130  lsatcv0  35153  lsat0cv  35155  lcv1  35163  l1cvpat  35176  dih1dimatlem  37453  dihatexv2  37463  djhcvat42  37539  dihjat1lem  37552  dochsatshp  37575  lcfl6  37624  mapdrvallem2  37769  mapdpglem32  37829
  Copyright terms: Public domain W3C validator