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

Theorem eldifi 3593
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 3452 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 461 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1870    \ cdif 3439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-dif 3445
This theorem is referenced by:  difss  3598  noel  3771  eqoreldif  4044  xpdifid  5285  tz7.7  5468  tfi  6694  peano5  6730  wfrlem10  7053  wfrlem15  7058  tz7.48-1  7168  tz7.49  7170  dif20el  7215  oaf1o  7272  oeordi  7296  oeord  7297  oecan  7298  oeword  7299  oeworde  7302  oelimcl  7309  oeeulem  7310  oeeui  7311  oaabs2  7354  boxcutc  7573  domdifsn  7661  isinf  7791  pssnn  7796  pwfilem  7874  fsuppco2  7922  fsuppcor  7923  ordtypelem7  8039  unxpwdom2  8103  inf3lem3  8135  cantnfp1lem1  8182  cantnfp1lem3  8184  infxpenc2lem1  8448  dfacacn  8569  isf32lem3  8783  isf34lem4  8805  fin67  8823  isfin7-2  8824  domtriomlem  8870  axdc2lem  8876  axdc3lem4  8881  axdc4lem  8883  ttukeylem7  8943  konigthlem  8991  fpwwe2lem13  9066  fpwwe2  9067  hashf1lem1  12613  rlimrege0  13621  rlimrecl  13622  sumrblem  13755  fsumcvg  13756  summolem2a  13759  fsumss  13769  fsumless  13834  cvgcmpce  13856  binomlem  13865  incexclem  13872  incexc  13873  isumltss  13884  prodrblem  13961  fprodcvg  13962  prodmolem2a  13966  fprodss  13980  fprodn0f  14023  fprodeq0g  14026  rpnnen2lem10  14254  rpnnen2lem11  14255  fproddvdsd  14348  lcmfunsnlem2  14584  oddprm  14728  iserodd  14748  prmreclem2  14824  prmreclem3  14825  prmreclem5  14827  4sqlem19  14876  prmdvdsprmo  14963  prmodvdslcmf  14968  prmdvdsprmorOLD  14978  prmordvdslcmfOLD  14982  prmordvdslcmsOLDOLD  14984  prmlem0  15040  firest  15290  grpinvnzcl  16677  symgextfv  17010  pmtrf  17047  pmtrdifellem3  17070  sylow2alem2  17205  sylow2a  17206  efgsf  17314  efgsrel  17319  efgs1  17320  efgsfo  17324  efgredlemc  17330  gsumzaddlem  17489  gsumzadd  17490  gsumzmhm  17505  gsum2d2lem  17540  dprdfadd  17588  dprdres  17596  subgdmdprd  17602  dmdprdsplitlem  17605  dmdprdsplit2lem  17613  dpjidcl  17626  ablfac1b  17638  pgpfac1lem1  17642  gsummgp0  17771  isirred  17862  irredrmul  17870  isdrng2  17920  isdrngd  17935  lcomfsupp  18063  lbspropd  18257  lspsneq  18280  lsppratlem6  18310  lbsextlem2  18317  lbsextlem4  18319  ringelnzr  18425  psrbaglesupp  18527  psrlidm  18562  psrridm  18563  mplsubglem  18593  mpllsslem  18594  mplsubrglem  18598  mplmonmul  18623  mplcoe1  18624  mplcoe5  18627  mplbas2  18629  evlslem3  18672  coe1tmmul2  18804  coe1tmmul  18805  xrs1mnd  18941  xrs10  18942  xrs1cmn  18943  cnsubrg  18963  psgnodpm  19087  zrhpsgnodpm  19091  evpmodpmf1o  19095  uvcresum  19282  frlmssuvc1  19283  frlmsslsp  19285  frlmup2  19288  lindfrn  19310  f1lindf  19311  lindfmm  19316  islindf4  19327  dmatmul  19453  1marepvsma1  19539  mdetdiaglem  19554  mdetrlin  19558  mdetrsca  19559  mdetralt  19564  maducoeval2  19596  madugsum  19599  symgmatr01  19610  gsummatr01lem3  19613  gsummatr01lem4  19614  gsummatr01  19615  smadiadetlem0  19617  smadiadetlem1a  19619  cmpfi  20354  2ndcdisj2  20403  elptr2  20520  ptcnplem  20567  xkopt  20601  kqdisj  20678  fin1aufil  20878  ptcmplem2  20999  ptcmplem3  21000  ptcmplem4  21001  opnsubg  21053  lpbl  21449  blcld  21451  zcld  21742  recld2  21743  reconnlem1  21755  divcn  21796  iundisj  22378  mbfeqalem  22475  itg1val2  22519  itg1ge0  22521  i1fmullem  22529  i1fadd  22530  itg1addlem4  22534  itg1mulc  22539  itg1lea  22547  itg1le  22548  mbfi1fseqlem4  22553  itg2uba  22578  itg2lea  22579  itg2eqa  22580  itg2splitlem  22583  itg2split  22584  itgeqa  22648  ellimc3  22711  dvaddbr  22769  dvmulbr  22770  dvcobr  22777  dvcjbr  22780  dvrec  22786  dvcnvlem  22805  dvexp3  22807  dveflem  22808  tdeglem4  22886  deg1n0ima  22915  deg1mul3le  22942  ig1peu  22997  ply1termlem  23025  plypf1  23034  plyaddlem1  23035  plymullem1  23036  coeeulem  23046  coeidlem  23059  coeid3  23062  coefv0  23070  coemulhi  23076  coemulc  23077  dvply1  23105  fta1  23129  vieta1lem2  23132  elaa  23137  elqaalem2  23141  aannenlem2  23150  aaliou2  23161  tayl0  23182  dvtaylp  23190  taylthlem1  23193  taylthlem2  23194  pserdvlem2  23248  logbcl  23569  relogbreexp  23577  relogbcxp  23587  cxplogb  23588  dcubic  23637  rlimcnp  23756  jensen  23779  dmgmaddn0  23813  dmlogdmgm  23814  lgamgulmlem2  23820  igamz  23838  gamp1  23848  regamcl  23851  wilthlem2  23859  basellem3  23872  chpub  24011  logexprlim  24016  lgslem1  24087  lgslem4  24090  lgsvalmod  24106  lgsqr  24137  lgsquadlem1  24145  lgsquad2  24151  m1lgs  24153  dchrisum0fno1  24212  rplogsum  24228  ishpg  24657  cusgraexi  25041  uvtxnbgra  25066  cusconngra  25249  frgrancvvdeqlem9  25614  frgrancvvdeq  25615  frgrancvvdgeq  25616  2spotiundisj  25635  frghash2spot  25636  ablomul  25928  mulid  25929  zerdivemp1  26007  strlem1  27738  strlem3  27741  strlem4  27742  strlem5  27743  hstrlem3  27749  hstrlem4  27750  iundisjf  28038  suppss3  28155  iundisjfi  28208  qtophaus  28502  elzdif0  28623  ind0  28680  measvunilem  28873  sibfof  29001  eulerpartlemb  29027  eulerpartlemf  29029  sseqf  29051  ballotlem5  29158  ballotlemi1  29161  ballotlemii  29162  ballotlemic  29165  ballotlem1c  29166  ballotlemscr  29177  ballotlemro  29181  ballotlemfg  29184  ballotlemfrc  29185  ballotlemfrceq  29187  ballotlemrinv0  29191  plymulx0  29224  signstfvn  29246  bnj923  29367  bnj570  29504  bnj594  29511  subfacp1lem1  29690  mrsubcn  29945  mrsubco  29947  circum  30106  dfon2lem6  30221  neibastop1  30800  poimirlem24  31668  poimirlem25  31669  dvtan  31696  itg2addnclem2  31698  ftc1cnnc  31720  dvasin  31732  dvreasin  31734  dvreacos  31735  isdrngo2  31901  isdrngo3  31902  divrngidl  31965  isfldidl  32005  pridlc2  32009  pridlc3  32010  prter2  32161  lsateln0  32270  lsatlss  32271  lsmsat  32283  lsatcv0  32306  lsat0cv  32308  lcv1  32316  l1cvpat  32329  dih1dimatlem  34606  dihatexv2  34616  djhcvat42  34692  dihjat1lem  34705  dochsatshp  34728  lcfl6  34777  mapdrvallem2  34922  mapdpglem32  34982  irrapx1  35382  pell1234qrne0  35407  pell1234qrreccl  35408  pell1234qrmulcl  35409  pell14qrgt0  35413  pell1234qrdich  35415  pell14qrdich  35423  pell1qrge1  35424  pell1qr1  35425  pell1qrgap  35428  pell14qrgapw  35430  pellqrexplicit  35431  pellqrex  35433  pellfundge  35436  pellfundgt1  35437  setindtr  35585  kelac1  35627  mpaaeu  35715  flcidc  35739  cntzsdrg  35767  deg1mhm  35783  radcnvrat  36300  binomcxplemdvbinom  36339  disjiun2  37039  fiiuncl  37048  disjf1o  37089  icoiccdif  37210  fsumnncl  37225  fsumsplit1  37226  fprod0  37248  climrec  37253  islpcn  37291  lptre2pt  37292  limclner  37304  fprodcncf  37351  dvrecg  37354  fperdvper  37362  dvdivcncf  37371  dvnmul  37387  dvmptfprodlem  37388  dvnprodlem2  37391  stoweidlem25  37454  stoweidlem28  37457  stoweidlem41  37471  stoweidlem44  37474  stoweidlem46  37476  stirlinglem5  37509  dirkercncflem1  37534  dirkercncflem2  37535  fourierdlem24  37562  fourierdlem62  37600  fouriersw  37663  fouriercn  37664  elaa2lem  37665  elaa2  37666  etransclem25  37691  etransclem35  37701  etransclem44  37710  sge0iunmptlemfi  37789  sge0fodjrnlem  37792  iundjiunlem  37806  meadjiunlem  37812  bgoldbtbndlem2  38291  bgoldbtbndlem3  38292  bgoldbtbndlem4  38293  bgoldbtbnd  38294  fsummsndifre  38415  fsummmodsndifre  38417  c0rhm  38670  c0rnghm  38671  zrrnghm  38675  2zrngnmlid2  38709  zrinitorngc  38760  zrtermorngc  38761  mgpsumunsn  38903  mgpsumz  38904  mgpsumn  38905  lindslinindsimp1  39010  lindslinindsimp2  39016  lincresunit1  39030  lincresunit2  39031  lincresunit3lem1  39032  lincresunit3lem2  39033  lincresunit3  39034  lindssnlvec  39039  logcxp0  39107  relogbmulbexp  39133  relogbdivb  39134  dignn0fr  39173
  Copyright terms: Public domain W3C validator