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

Theorem eldifi 3470
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 3331 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 448 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1726    \ cdif 3318
This theorem is referenced by:  difss  3475  noel  3633  tz7.7  4608  tfi  4834  peano5  4869  tz7.48-1  6701  tz7.49  6703  dif20el  6750  oaf1o  6807  oeordi  6831  oeord  6832  oecan  6833  oeword  6834  oeworde  6837  oelimcl  6844  oeeulem  6845  oeeui  6846  oaabs2  6889  boxcutc  7106  domdifsn  7192  isinf  7323  pssnn  7328  pwfilem  7402  ordtypelem7  7494  unxpwdom2  7557  inf3lem3  7586  cantnfp1lem1  7635  cantnfp1lem3  7637  infxpenc2lem1  7901  dfacacn  8022  isf32lem3  8236  isf34lem4  8258  fin67  8276  isfin7-2  8277  domtriomlem  8323  axdc2lem  8329  axdc3lem4  8334  axdc4lem  8336  ttukeylem7  8396  konigthlem  8444  fpwwe2lem13  8518  fpwwe2  8519  hashf1lem1  11705  rlimrege0  12374  rlimrecl  12375  sumrblem  12506  fsumcvg  12507  summolem2a  12510  fsumss  12520  fsumless  12576  cvgcmpce  12598  binomlem  12609  incexclem  12617  incexc  12618  isumltss  12629  rpnnen2lem10  12824  rpnnen2lem11  12825  oddprm  13190  iserodd  13210  prmreclem2  13286  prmreclem3  13287  prmreclem5  13289  4sqlem19  13332  prmlem0  13429  firest  13661  grpinvnzcl  14864  sylow2alem2  15253  sylow2a  15254  efgsf  15362  efgsrel  15367  efgs1  15368  efgsfo  15372  efgredlemc  15378  gsumzaddlem  15527  gsumzadd  15528  gsumzmhm  15534  gsumzinv  15541  gsumsub  15543  gsum2d2lem  15548  dprdfadd  15579  dprdsubg  15583  dprdres  15587  subgdmdprd  15593  dmdprdsplitlem  15596  dmdprdsplit2lem  15604  dpjidcl  15617  ablfac1b  15629  pgpfac1lem1  15633  isirred  15805  irredrmul  15813  isdrng2  15846  isdrngd  15861  lbspropd  16172  lspsneq  16195  lsppratlem6  16225  lbsextlem2  16232  lbsextlem4  16234  rngelnzr  16337  psrbaglesupp  16434  psrlidm  16468  psrridm  16469  mplsubglem  16499  mpllsslem  16500  mplsubrglem  16503  mplmonmul  16528  mplcoe1  16529  mplcoe2  16531  mplbas2  16532  coe1tmmul2  16669  coe1tmmul  16670  xrs1mnd  16737  xrs10  16738  xrs1cmn  16739  cnsubrg  16760  cmpfi  17472  2ndcdisj2  17521  elptr2  17607  ptcnplem  17654  xkopt  17688  kqdisj  17765  fin1aufil  17965  ptcmplem2  18085  ptcmplem3  18086  ptcmplem4  18087  opnsubg  18138  lpbl  18534  blcld  18536  zcld  18845  recld2  18846  reconnlem1  18858  divcn  18899  iundisj  19443  mbfeqalem  19535  itg1val2  19577  itg1ge0  19579  i1fmullem  19587  i1fadd  19588  itg1addlem4  19592  itg1mulc  19597  itg1lea  19605  itg1le  19606  mbfi1fseqlem4  19611  itg2uba  19636  itg2lea  19637  itg2eqa  19638  itg2splitlem  19641  itg2split  19642  itgeqa  19706  ellimc3  19767  dvaddbr  19825  dvmulbr  19826  dvcobr  19833  dvcjbr  19836  dvrec  19842  dvcnvlem  19861  dvexp3  19863  dveflem  19864  evlslem3  19936  tdeglem4  19984  mdeg0  19994  deg1n0ima  20013  deg1mul3le  20040  ig1peu  20095  ply1termlem  20123  plypf1  20132  plyaddlem1  20133  plymullem1  20134  coeeulem  20144  coeidlem  20157  coeid3  20160  coefv0  20167  coemulhi  20173  coemulc  20174  dvply1  20202  fta1  20226  vieta1lem2  20229  elaa  20234  elqaalem2  20238  aannenlem2  20247  aaliou2  20258  tayl0  20279  dvtaylp  20287  taylthlem1  20290  taylthlem2  20291  pserdvlem2  20345  dcubic  20687  rlimcnp  20805  jensen  20828  wilthlem2  20853  basellem3  20866  chpub  21005  logexprlim  21010  lgslem1  21081  lgslem4  21084  lgsvalmod  21100  lgsqr  21131  lgsquadlem1  21139  lgsquad2  21145  m1lgs  21147  dchrisum0fno1  21206  rplogsum  21222  cusgraexi  21478  uvtxnbgra  21503  cusconngra  21664  ablomul  21944  mulid  21945  zerdivemp1  22023  strlem1  23754  strlem3  23757  strlem4  23758  strlem5  23759  hstrlem3  23765  hstrlem4  23766  iundisjf  24030  iundisjfi  24153  elzdif0  24365  logbcl  24398  ind0  24418  measvunilem  24567  ballotlem5  24758  ballotlemi1  24761  ballotlemii  24762  ballotlemic  24765  ballotlem1c  24766  ballotlemscr  24777  ballotlemro  24781  ballotlemfg  24784  ballotlemfrc  24785  ballotlemfrceq  24787  ballotlemrinv0  24791  dmgmaddn0  24808  dmlogdmgm  24809  lgamgulmlem2  24815  igamz  24833  gamp1  24843  regamcl  24846  subfacp1lem1  24866  circum  25112  prodrblem  25256  fprodcvg  25257  prodmolem2a  25261  fprodss  25275  dfon2lem6  25416  wfrlem10  25548  wfrlem15  25553  itg2addnclem2  26258  ftc1cnnc  26280  dvreasin  26291  neibastop1  26389  isdrngo2  26575  isdrngo3  26576  divrngidl  26639  isfldidl  26679  pridlc2  26683  pridlc3  26684  prter2  26731  lcomfsup  26748  irrapx1  26892  pell1234qrne0  26917  pell1234qrreccl  26918  pell1234qrmulcl  26919  pell14qrgt0  26923  pell1234qrdich  26925  pell14qrdich  26933  pell1qrge1  26934  pell1qr1  26935  pell1qrgap  26938  pell14qrgapw  26940  pellqrexplicit  26941  pellqrex  26943  pellfundge  26946  pellfundgt1  26947  setindtr  27096  kelac1  27139  uvcresum  27220  frlmssuvc1  27224  frlmsslsp  27226  frlmup1  27228  frlmup2  27229  lindfrn  27269  f1lindf  27270  lindfmm  27275  islindf4  27286  mpaaeu  27333  flcidc  27357  pmtrf  27375  mamulid  27436  mamurid  27437  cntzsdrg  27488  deg1mhm  27504  climrec  27706  stoweidlem25  27751  stoweidlem28  27754  stoweidlem41  27767  stoweidlem44  27770  stoweidlem46  27772  stirlinglem5  27804  frgrancvvdeqlem9  28431  frgrancvvdeq  28432  frgrancvvdgeq  28433  2spotiundisj  28452  frghash2spot  28453  elogb  28533  bnj923  29138  bnj570  29277  bnj594  29284  lsateln0  29794  lsatlss  29795  lsmsat  29807  lsatcv0  29830  lsat0cv  29832  lcv1  29840  l1cvpat  29853  dih1dimatlem  32128  dihatexv2  32138  djhcvat42  32214  dihjat1lem  32227  dochsatshp  32250  lcfl6  32299  mapdrvallem2  32444  mapdpglem32  32504  mapdh9aOLDN  32590  hdmap1eulemOLDN  32624
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-dif 3324
  Copyright terms: Public domain W3C validator