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

Theorem eldifi 3466
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 3326 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 457 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1755    \ cdif 3313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319
This theorem is referenced by:  difss  3471  noel  3629  tz7.7  4732  tfi  6453  peano5  6488  tz7.48-1  6884  tz7.49  6886  dif20el  6933  oaf1o  6990  oeordi  7014  oeord  7015  oecan  7016  oeword  7017  oeworde  7020  oelimcl  7027  oeeulem  7028  oeeui  7029  oaabs2  7072  boxcutc  7294  domdifsn  7382  isinf  7514  pssnn  7519  pwfilem  7593  fsuppco2  7640  fsuppcor  7641  ordtypelem7  7726  unxpwdom2  7791  inf3lem3  7824  cantnfp1lem1  7874  cantnfp1lem3  7876  cantnfp1lem1OLD  7900  cantnfp1lem3OLD  7902  infxpenc2lem1  8173  dfacacn  8298  isf32lem3  8512  isf34lem4  8534  fin67  8552  isfin7-2  8553  domtriomlem  8599  axdc2lem  8605  axdc3lem4  8610  axdc4lem  8612  ttukeylem7  8672  konigthlem  8720  fpwwe2lem13  8796  fpwwe2  8797  hashf1lem1  12191  rlimrege0  13040  rlimrecl  13041  sumrblem  13171  fsumcvg  13172  summolem2a  13175  fsumss  13185  fsumless  13241  cvgcmpce  13263  binomlem  13274  incexclem  13281  incexc  13282  isumltss  13293  rpnnen2lem10  13488  rpnnen2lem11  13489  oddprm  13864  iserodd  13884  prmreclem2  13960  prmreclem3  13961  prmreclem5  13963  4sqlem19  14006  prmlem0  14115  firest  14353  grpinvnzcl  15577  symgextfv  15902  pmtrf  15940  pmtrdifellem3  15963  sylow2alem2  16096  sylow2a  16097  efgsf  16205  efgsrel  16210  efgs1  16211  efgsfo  16215  efgredlemc  16221  gsumzaddlem  16387  gsumzadd  16388  gsumzaddlemOLD  16389  gsumzaddOLD  16390  gsumzmhm  16406  gsumzmhmOLD  16407  gsumzinvOLD  16418  gsumsubOLD  16423  gsum2d2lem  16438  dprdfadd  16483  dprdfaddOLD  16490  dprdres  16498  subgdmdprd  16504  dmdprdsplitlem  16507  dmdprdsplitlemOLD  16508  dmdprdsplit2lem  16517  dpjidcl  16530  dpjidclOLD  16537  ablfac1b  16544  pgpfac1lem1  16548  gsummgp0  16633  isirred  16724  irredrmul  16732  isdrng2  16765  isdrngd  16780  lcomfsupOLD  16907  lcomfsupp  16908  lbspropd  17101  lspsneq  17124  lsppratlem6  17154  lbsextlem2  17161  lbsextlem4  17163  rngelnzr  17268  psrbaglesupp  17368  psrbaglesuppOLD  17369  psrlidm  17407  psrlidmOLD  17408  psrridm  17409  psrridmOLD  17410  mplsubglem  17443  mpllsslem  17444  mplsubglemOLD  17445  mpllsslemOLD  17446  mplsubrglem  17450  mplsubrglemOLD  17451  mplmonmul  17476  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  mplbas2  17482  mplbas2OLD  17483  coe1tmmul2  17626  coe1tmmul  17627  xrs1mnd  17694  xrs10  17695  xrs1cmn  17696  cnsubrg  17716  psgnodpm  17859  zrhpsgnodpm  17863  evpmodpmf1o  17867  uvcresum  18059  frlmssuvc1  18060  frlmssuvc1OLD  18062  frlmsslsp  18064  frlmsslspOLD  18065  frlmup2  18068  lindfrn  18091  f1lindf  18092  lindfmm  18097  islindf4  18108  1marepvsma1  18235  mdet1  18249  mdetrlin  18250  mdetrsca  18251  mdetralt  18255  maducoeval2  18287  madugsum  18290  symgmatr01  18301  gsummatr01lem3  18304  gsummatr01lem4  18305  gsummatr01  18306  smadiadetlem0  18308  smadiadetlem1a  18310  cmpfi  18852  2ndcdisj2  18902  elptr2  18988  ptcnplem  19035  xkopt  19069  kqdisj  19146  fin1aufil  19346  ptcmplem2  19466  ptcmplem3  19467  ptcmplem4  19468  opnsubg  19519  lpbl  19919  blcld  19921  zcld  20231  recld2  20232  reconnlem1  20244  divcn  20285  iundisj  20870  mbfeqalem  20961  itg1val2  21003  itg1ge0  21005  i1fmullem  21013  i1fadd  21014  itg1addlem4  21018  itg1mulc  21023  itg1lea  21031  itg1le  21032  mbfi1fseqlem4  21037  itg2uba  21062  itg2lea  21063  itg2eqa  21064  itg2splitlem  21067  itg2split  21068  itgeqa  21132  ellimc3  21195  dvaddbr  21253  dvmulbr  21254  dvcobr  21261  dvcjbr  21264  dvrec  21270  dvcnvlem  21289  dvexp3  21291  dveflem  21292  evlslem3  21365  tdeglem4  21413  deg1n0ima  21444  deg1mul3le  21472  ig1peu  21527  ply1termlem  21555  plypf1  21564  plyaddlem1  21565  plymullem1  21566  coeeulem  21576  coeidlem  21589  coeid3  21592  coefv0  21599  coemulhi  21605  coemulc  21606  dvply1  21634  fta1  21658  vieta1lem2  21661  elaa  21666  elqaalem2  21670  aannenlem2  21679  aaliou2  21690  tayl0  21711  dvtaylp  21719  taylthlem1  21722  taylthlem2  21723  pserdvlem2  21777  dcubic  22125  rlimcnp  22243  jensen  22266  wilthlem2  22291  basellem3  22304  chpub  22443  logexprlim  22448  lgslem1  22519  lgslem4  22522  lgsvalmod  22538  lgsqr  22569  lgsquadlem1  22577  lgsquad2  22583  m1lgs  22585  dchrisum0fno1  22644  rplogsum  22660  cusgraexi  23198  uvtxnbgra  23223  cusconngra  23384  ablomul  23664  mulid  23665  zerdivemp1  23743  strlem1  25476  strlem3  25479  strlem4  25480  strlem5  25481  hstrlem3  25487  hstrlem4  25488  iundisjf  25754  iundisjfi  25902  elzdif0  26262  logbcl  26309  ind0  26329  measvunilem  26479  eulerpartlemb  26598  eulerpartlemf  26600  sseqf  26622  ballotlem5  26729  ballotlemi1  26732  ballotlemii  26733  ballotlemic  26736  ballotlem1c  26737  ballotlemscr  26748  ballotlemro  26752  ballotlemfg  26755  ballotlemfrc  26756  ballotlemfrceq  26758  ballotlemrinv0  26762  plymulx0  26795  signstfvn  26817  dmgmaddn0  26856  dmlogdmgm  26857  lgamgulmlem2  26863  igamz  26881  gamp1  26891  regamcl  26894  subfacp1lem1  26914  circum  27165  prodrblem  27288  fprodcvg  27289  prodmolem2a  27293  fprodss  27307  dfon2lem6  27447  wfrlem10  27579  wfrlem15  27584  dvtan  28283  itg2addnclem2  28285  ftc1cnnc  28307  dvasin  28321  dvreasin  28323  dvreacos  28324  neibastop1  28421  isdrngo2  28605  isdrngo3  28606  divrngidl  28669  isfldidl  28709  pridlc2  28713  pridlc3  28714  prter2  28868  irrapx1  29011  pell1234qrne0  29036  pell1234qrreccl  29037  pell1234qrmulcl  29038  pell14qrgt0  29042  pell1234qrdich  29044  pell14qrdich  29052  pell1qrge1  29053  pell1qr1  29054  pell1qrgap  29057  pell14qrgapw  29059  pellqrexplicit  29060  pellqrex  29062  pellfundge  29065  pellfundgt1  29066  setindtr  29215  kelac1  29258  mpaaeu  29349  flcidc  29373  cntzsdrg  29401  deg1mhm  29417  climrec  29619  stoweidlem25  29663  stoweidlem28  29666  stoweidlem41  29679  stoweidlem44  29682  stoweidlem46  29684  stirlinglem5  29716  fsummsndifre  30080  fsummmodsndifre  30082  frgrancvvdeqlem9  30477  frgrancvvdeq  30478  frgrancvvdgeq  30479  2spotiundisj  30498  frghash2spot  30499  mgpsumunsn  30590  mgpsumz  30591  mgpsumn  30592  lindslinindsimp1  30697  lindslinindsimp2  30703  lincresunit1  30717  lincresunit2  30718  lincresunit3lem1  30719  lincresunit3lem2  30720  lincresunit3  30721  lindssnlvec  30726  elogb  30816  bnj923  31460  bnj570  31597  bnj594  31604  lsateln0  32210  lsatlss  32211  lsmsat  32223  lsatcv0  32246  lsat0cv  32248  lcv1  32256  l1cvpat  32269  dih1dimatlem  34544  dihatexv2  34554  djhcvat42  34630  dihjat1lem  34643  dochsatshp  34666  lcfl6  34715  mapdrvallem2  34860  mapdpglem32  34920  mapdh9aOLDN  35006  hdmap1eulemOLDN  35040
  Copyright terms: Public domain W3C validator