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

Theorem eldifi 3626
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 3486 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 460 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1767    \ cdif 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479
This theorem is referenced by:  difss  3631  noel  3789  tz7.7  4904  tfi  6666  peano5  6701  tz7.48-1  7105  tz7.49  7107  dif20el  7152  oaf1o  7209  oeordi  7233  oeord  7234  oecan  7235  oeword  7236  oeworde  7239  oelimcl  7246  oeeulem  7247  oeeui  7248  oaabs2  7291  boxcutc  7509  domdifsn  7597  isinf  7730  pssnn  7735  pwfilem  7810  fsuppco2  7858  fsuppcor  7859  ordtypelem7  7945  unxpwdom2  8010  inf3lem3  8043  cantnfp1lem1  8093  cantnfp1lem3  8095  cantnfp1lem1OLD  8119  cantnfp1lem3OLD  8121  infxpenc2lem1  8392  dfacacn  8517  isf32lem3  8731  isf34lem4  8753  fin67  8771  isfin7-2  8772  domtriomlem  8818  axdc2lem  8824  axdc3lem4  8829  axdc4lem  8831  ttukeylem7  8891  konigthlem  8939  fpwwe2lem13  9016  fpwwe2  9017  hashf1lem1  12466  rlimrege0  13361  rlimrecl  13362  sumrblem  13492  fsumcvg  13493  summolem2a  13496  fsumss  13506  fsumless  13569  cvgcmpce  13591  binomlem  13600  incexclem  13607  incexc  13608  isumltss  13619  rpnnen2lem10  13814  rpnnen2lem11  13815  oddprm  14194  iserodd  14214  prmreclem2  14290  prmreclem3  14291  prmreclem5  14293  4sqlem19  14336  prmlem0  14445  firest  14684  grpinvnzcl  15911  symgextfv  16238  pmtrf  16276  pmtrdifellem3  16299  sylow2alem2  16434  sylow2a  16435  efgsf  16543  efgsrel  16548  efgs1  16549  efgsfo  16553  efgredlemc  16559  gsumzaddlem  16725  gsumzadd  16726  gsumzaddlemOLD  16727  gsumzaddOLD  16728  gsumzmhm  16748  gsumzmhmOLD  16749  gsumzinvOLD  16761  gsumsubOLD  16766  gsum2d2lem  16792  dprdfadd  16850  dprdfaddOLD  16857  dprdres  16865  subgdmdprd  16871  dmdprdsplitlem  16874  dmdprdsplitlemOLD  16875  dmdprdsplit2lem  16884  dpjidcl  16897  dpjidclOLD  16904  ablfac1b  16911  pgpfac1lem1  16915  gsummgp0  17040  isirred  17132  irredrmul  17140  isdrng2  17189  isdrngd  17204  lcomfsupOLD  17332  lcomfsupp  17333  lbspropd  17528  lspsneq  17551  lsppratlem6  17581  lbsextlem2  17588  lbsextlem4  17590  rngelnzr  17695  psrbaglesupp  17788  psrbaglesuppOLD  17789  psrlidm  17827  psrlidmOLD  17828  psrridm  17829  psrridmOLD  17830  mplsubglem  17864  mpllsslem  17865  mplsubglemOLD  17866  mpllsslemOLD  17867  mplsubrglem  17871  mplsubrglemOLD  17872  mplmonmul  17897  mplcoe1  17898  mplcoe5  17902  mplcoe2OLD  17904  mplbas2  17905  mplbas2OLD  17906  evlslem3  17954  coe1tmmul2  18088  coe1tmmul  18089  xrs1mnd  18224  xrs10  18225  xrs1cmn  18226  cnsubrg  18246  psgnodpm  18391  zrhpsgnodpm  18395  evpmodpmf1o  18399  uvcresum  18591  frlmssuvc1  18592  frlmssuvc1OLD  18594  frlmsslsp  18596  frlmsslspOLD  18597  frlmup2  18600  lindfrn  18623  f1lindf  18624  lindfmm  18629  islindf4  18640  dmatmul  18766  1marepvsma1  18852  mdetdiaglem  18867  mdetrlin  18871  mdetrsca  18872  mdetralt  18877  maducoeval2  18909  madugsum  18912  symgmatr01  18923  gsummatr01lem3  18926  gsummatr01lem4  18927  gsummatr01  18928  smadiadetlem0  18930  smadiadetlem1a  18932  cmpfi  19674  2ndcdisj2  19724  elptr2  19810  ptcnplem  19857  xkopt  19891  kqdisj  19968  fin1aufil  20168  ptcmplem2  20288  ptcmplem3  20289  ptcmplem4  20290  opnsubg  20341  lpbl  20741  blcld  20743  zcld  21053  recld2  21054  reconnlem1  21066  divcn  21107  iundisj  21693  mbfeqalem  21784  itg1val2  21826  itg1ge0  21828  i1fmullem  21836  i1fadd  21837  itg1addlem4  21841  itg1mulc  21846  itg1lea  21854  itg1le  21855  mbfi1fseqlem4  21860  itg2uba  21885  itg2lea  21886  itg2eqa  21887  itg2splitlem  21890  itg2split  21891  itgeqa  21955  ellimc3  22018  dvaddbr  22076  dvmulbr  22077  dvcobr  22084  dvcjbr  22087  dvrec  22093  dvcnvlem  22112  dvexp3  22114  dveflem  22115  tdeglem4  22193  deg1n0ima  22224  deg1mul3le  22252  ig1peu  22307  ply1termlem  22335  plypf1  22344  plyaddlem1  22345  plymullem1  22346  coeeulem  22356  coeidlem  22369  coeid3  22372  coefv0  22379  coemulhi  22385  coemulc  22386  dvply1  22414  fta1  22438  vieta1lem2  22441  elaa  22446  elqaalem2  22450  aannenlem2  22459  aaliou2  22470  tayl0  22491  dvtaylp  22499  taylthlem1  22502  taylthlem2  22503  pserdvlem2  22557  dcubic  22905  rlimcnp  23023  jensen  23046  wilthlem2  23071  basellem3  23084  chpub  23223  logexprlim  23228  lgslem1  23299  lgslem4  23302  lgsvalmod  23318  lgsqr  23349  lgsquadlem1  23357  lgsquad2  23363  m1lgs  23365  dchrisum0fno1  23424  rplogsum  23440  cusgraexi  24144  uvtxnbgra  24169  cusconngra  24352  frgrancvvdeqlem9  24718  frgrancvvdeq  24719  frgrancvvdgeq  24720  2spotiundisj  24739  frghash2spot  24740  ablomul  25033  mulid  25034  zerdivemp1  25112  strlem1  26845  strlem3  26848  strlem4  26849  strlem5  26850  hstrlem3  26856  hstrlem4  26857  iundisjf  27121  iundisjfi  27269  elzdif0  27597  logbcl  27653  ind0  27673  measvunilem  27823  eulerpartlemb  27947  eulerpartlemf  27949  sseqf  27971  ballotlem5  28078  ballotlemi1  28081  ballotlemii  28082  ballotlemic  28085  ballotlem1c  28086  ballotlemscr  28097  ballotlemro  28101  ballotlemfg  28104  ballotlemfrc  28105  ballotlemfrceq  28107  ballotlemrinv0  28111  plymulx0  28144  signstfvn  28166  dmgmaddn0  28205  dmlogdmgm  28206  lgamgulmlem2  28212  igamz  28230  gamp1  28240  regamcl  28243  subfacp1lem1  28263  circum  28515  prodrblem  28638  fprodcvg  28639  prodmolem2a  28643  fprodss  28657  dfon2lem6  28797  wfrlem10  28929  wfrlem15  28934  dvtan  29642  itg2addnclem2  29644  ftc1cnnc  29666  dvasin  29680  dvreasin  29682  dvreacos  29683  neibastop1  29780  isdrngo2  29964  isdrngo3  29965  divrngidl  30028  isfldidl  30068  pridlc2  30072  pridlc3  30073  prter2  30226  irrapx1  30368  pell1234qrne0  30393  pell1234qrreccl  30394  pell1234qrmulcl  30395  pell14qrgt0  30399  pell1234qrdich  30401  pell14qrdich  30409  pell1qrge1  30410  pell1qr1  30411  pell1qrgap  30414  pell14qrgapw  30416  pellqrexplicit  30417  pellqrex  30419  pellfundge  30422  pellfundgt1  30423  setindtr  30570  kelac1  30613  mpaaeu  30704  flcidc  30728  cntzsdrg  30756  deg1mhm  30772  climrec  31145  islpcn  31181  lptre2pt  31182  limclner  31193  dvrecg  31240  fperdvper  31248  dvdivcncf  31257  stoweidlem25  31325  stoweidlem28  31328  stoweidlem41  31341  stoweidlem44  31344  stoweidlem46  31346  stirlinglem5  31378  dirkercncflem1  31403  dirkercncflem2  31404  fourierdlem24  31431  fourierdlem62  31469  fouriersw  31532  fouriercn  31533  fsummsndifre  31814  fsummmodsndifre  31816  mgpsumunsn  32015  mgpsumz  32016  mgpsumn  32017  lindslinindsimp1  32131  lindslinindsimp2  32137  lincresunit1  32151  lincresunit2  32152  lincresunit3lem1  32153  lincresunit3lem2  32154  lincresunit3  32155  lindssnlvec  32160  elogb  32250  bnj923  32905  bnj570  33042  bnj594  33049  lsateln0  33792  lsatlss  33793  lsmsat  33805  lsatcv0  33828  lsat0cv  33830  lcv1  33838  l1cvpat  33851  dih1dimatlem  36126  dihatexv2  36136  djhcvat42  36212  dihjat1lem  36225  dochsatshp  36248  lcfl6  36297  mapdrvallem2  36442  mapdpglem32  36502  mapdh9aOLDN  36588  hdmap1eulemOLDN  36622
  Copyright terms: Public domain W3C validator