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

Theorem eldifi 3523
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 3382 . 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 1872    \ cdif 3369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-v 3018  df-dif 3375
This theorem is referenced by:  difss  3528  noel  3701  eqoreldif  3977  xpdifid  5220  tz7.7  5404  tfi  6631  peano5  6667  wfrlem10  6993  wfrlem15  6998  tz7.48-1  7108  tz7.49  7110  dif20el  7155  oaf1o  7212  oeordi  7236  oeord  7237  oecan  7238  oeword  7239  oeworde  7242  oelimcl  7249  oeeulem  7250  oeeui  7251  oaabs2  7294  boxcutc  7513  domdifsn  7601  isinf  7731  pssnn  7736  pwfilem  7814  fsuppco2  7862  fsuppcor  7863  ordtypelem7  7985  unxpwdom2  8049  inf3lem3  8081  cantnfp1lem1  8128  cantnfp1lem3  8130  infxpenc2lem1  8394  dfacacn  8515  isf32lem3  8729  isf34lem4  8751  fin67  8769  isfin7-2  8770  domtriomlem  8816  axdc2lem  8822  axdc3lem4  8827  axdc4lem  8829  ttukeylem7  8889  konigthlem  8937  fpwwe2lem13  9011  fpwwe2  9012  hashf1lem1  12559  rlimrege0  13579  rlimrecl  13580  sumrblem  13713  fsumcvg  13714  summolem2a  13717  fsumss  13727  fsumless  13792  cvgcmpce  13814  binomlem  13823  incexclem  13830  incexc  13831  isumltss  13842  prodrblem  13919  fprodcvg  13920  prodmolem2a  13924  fprodss  13938  fprodn0f  13981  fprodeq0g  13984  rpnnen2lem10  14212  rpnnen2lem11  14213  fproddvdsd  14306  lcmfunsnlem2  14549  oddprm  14701  iserodd  14721  prmreclem2  14797  prmreclem3  14798  prmreclem5  14800  4sqlem19  14849  prmdvdsprmo  14936  prmodvdslcmf  14941  prmdvdsprmorOLD  14951  prmordvdslcmfOLD  14955  prmordvdslcmsOLDOLD  14957  prmlem0  15013  firest  15267  grpinvnzcl  16662  symgextfv  16995  pmtrf  17032  pmtrdifellem3  17055  sylow2alem2  17206  sylow2a  17207  efgsf  17315  efgsrel  17320  efgs1  17321  efgsfo  17325  efgredlemc  17331  gsumzaddlem  17490  gsumzadd  17491  gsumzmhm  17506  gsum2d2lem  17541  dprdfadd  17589  dprdres  17597  subgdmdprd  17603  dmdprdsplitlem  17606  dmdprdsplit2lem  17614  dpjidcl  17627  ablfac1b  17639  pgpfac1lem1  17643  gsummgp0  17772  isirred  17863  irredrmul  17871  isdrng2  17921  isdrngd  17936  lcomfsupp  18064  lbspropd  18258  lspsneq  18281  lsppratlem6  18311  lbsextlem2  18318  lbsextlem4  18320  ringelnzr  18426  psrbaglesupp  18528  psrlidm  18563  psrridm  18564  mplsubglem  18594  mpllsslem  18595  mplsubrglem  18599  mplmonmul  18624  mplcoe1  18625  mplcoe5  18628  mplbas2  18630  evlslem3  18673  coe1tmmul2  18805  coe1tmmul  18806  xrs1mnd  18942  xrs10  18943  xrs1cmn  18944  cnsubrg  18964  psgnodpm  19091  zrhpsgnodpm  19095  evpmodpmf1o  19099  uvcresum  19286  frlmssuvc1  19287  frlmsslsp  19289  frlmup2  19292  lindfrn  19314  f1lindf  19315  lindfmm  19320  islindf4  19331  dmatmul  19457  1marepvsma1  19543  mdetdiaglem  19558  mdetrlin  19562  mdetrsca  19563  mdetralt  19568  maducoeval2  19600  madugsum  19603  symgmatr01  19614  gsummatr01lem3  19617  gsummatr01lem4  19618  gsummatr01  19619  smadiadetlem0  19621  smadiadetlem1a  19623  cmpfi  20358  2ndcdisj2  20407  elptr2  20524  ptcnplem  20571  xkopt  20605  kqdisj  20682  fin1aufil  20882  ptcmplem2  21003  ptcmplem3  21004  ptcmplem4  21005  opnsubg  21057  lpbl  21453  blcld  21455  zcld  21766  recld2  21767  reconnlem1  21779  divcn  21835  iundisj  22436  mbfeqalem  22533  itg1val2  22577  itg1ge0  22579  i1fmullem  22587  i1fadd  22588  itg1addlem4  22592  itg1mulc  22597  itg1lea  22605  itg1le  22606  mbfi1fseqlem4  22611  itg2uba  22636  itg2lea  22637  itg2eqa  22638  itg2splitlem  22641  itg2split  22642  itgeqa  22706  ellimc3  22769  dvaddbr  22827  dvmulbr  22828  dvcobr  22835  dvcjbr  22838  dvrec  22844  dvcnvlem  22863  dvexp3  22865  dveflem  22866  tdeglem4  22944  deg1n0ima  22973  deg1mul3le  23000  ig1peu  23057  ig1peuOLD  23058  ply1termlem  23092  plypf1  23101  plyaddlem1  23102  plymullem1  23103  coeeulem  23113  coeidlem  23126  coeid3  23129  coefv0  23137  coemulhi  23143  coemulc  23144  dvply1  23172  fta1  23196  vieta1lem2  23199  elaa  23204  elqaalem2  23208  elqaalem2OLD  23211  aannenlem2  23220  aaliou2  23231  tayl0  23252  dvtaylp  23260  taylthlem1  23263  taylthlem2  23264  pserdvlem2  23318  logbcl  23639  relogbreexp  23647  relogbcxp  23657  cxplogb  23658  dcubic  23707  rlimcnp  23826  jensen  23849  dmgmaddn0  23883  dmlogdmgm  23884  lgamgulmlem2  23890  igamz  23908  gamp1  23918  regamcl  23921  wilthlem2  23929  basellem3  23944  chpub  24083  logexprlim  24088  lgslem1  24159  lgslem4  24162  lgsvalmod  24178  lgsqr  24209  lgsquadlem1  24217  lgsquad2  24223  m1lgs  24225  dchrisum0fno1  24284  rplogsum  24300  ishpg  24736  cusgraexi  25131  uvtxnbgra  25156  cusconngra  25339  frgrancvvdeqlem9  25704  frgrancvvdeq  25705  frgrancvvdgeq  25706  2spotiundisj  25725  frghash2spot  25726  ablomul  26018  mulid  26019  zerdivemp1  26097  strlem1  27838  strlem3  27841  strlem4  27842  strlem5  27843  hstrlem3  27849  hstrlem4  27850  iundisjf  28138  suppss3  28255  iundisjfi  28315  qtophaus  28608  elzdif0  28729  ind0  28786  measvunilem  28979  sibfof  29118  eulerpartlemb  29146  eulerpartlemf  29148  sseqf  29170  ballotlem5  29277  ballotlemi1  29280  ballotlemii  29281  ballotlemic  29284  ballotlem1c  29285  ballotlemscr  29296  ballotlemro  29300  ballotlemfg  29303  ballotlemfrc  29304  ballotlemfrceq  29306  ballotlemrinv0  29310  ballotlemi1OLD  29318  ballotlemiiOLD  29319  ballotlemicOLD  29322  ballotlem1cOLD  29323  ballotlemscrOLD  29334  ballotlemroOLD  29338  ballotlemfgOLD  29341  ballotlemfrcOLD  29342  ballotlemfrceqOLD  29344  ballotlemrinv0OLD  29348  plymulx0  29381  signstfvn  29403  bnj923  29524  bnj570  29661  bnj594  29668  subfacp1lem1  29847  mrsubcn  30102  mrsubco  30104  circum  30263  dfon2lem6  30378  neibastop1  30957  poimirlem24  31865  poimirlem25  31866  dvtan  31893  itg2addnclem2  31895  ftc1cnnc  31917  dvasin  31929  dvreasin  31931  dvreacos  31932  isdrngo2  32098  isdrngo3  32099  divrngidl  32162  isfldidl  32202  pridlc2  32206  pridlc3  32207  prter2  32358  lsateln0  32467  lsatlss  32468  lsmsat  32480  lsatcv0  32503  lsat0cv  32505  lcv1  32513  l1cvpat  32526  dih1dimatlem  34803  dihatexv2  34813  djhcvat42  34889  dihjat1lem  34902  dochsatshp  34925  lcfl6  34974  mapdrvallem2  35119  mapdpglem32  35179  irrapx1  35579  pell1234qrne0  35606  pell1234qrreccl  35607  pell1234qrmulcl  35608  pell14qrgt0  35612  pell1234qrdich  35614  pell14qrdich  35622  pell1qrge1  35623  pell1qr1  35624  pell1qrgap  35627  pell14qrgapw  35629  pellqrexplicit  35630  pellqrex  35633  pellfundge  35637  pellfundgt1  35638  setindtr  35786  kelac1  35828  mpaaeu  35923  flcidc  35947  cntzsdrg  35975  deg1mhm  35991  radcnvrat  36570  binomcxplemdvbinom  36609  disjiun2  37308  fiiuncl  37316  disjf1o  37364  icoiccdif  37511  fsumnncl  37528  fsumsplit1  37529  fprod0  37553  climrec  37558  islpcn  37596  lptre2pt  37597  limclner  37609  fprodcncf  37656  dvrecg  37659  fperdvper  37667  dvdivcncf  37676  dvnmul  37695  dvmptfprodlem  37696  dvnprodlem2  37699  stoweidlem25  37762  stoweidlem28  37765  stoweidlem41  37779  stoweidlem44  37782  stoweidlem46  37784  stirlinglem5  37817  dirkercncflem1  37842  dirkercncflem2  37843  fourierdlem24  37870  fourierdlem62  37909  fouriersw  37972  fouriercn  37973  elaa2lem  37974  elaa2lemOLD  37975  elaa2  37976  etransclem25  38001  etransclem35  38011  etransclem44  38020  sge0iunmptlemfi  38100  sge0fodjrnlem  38103  iundjiunlem  38142  meadjiunlem  38148  isomenndlem  38196  hsphoidmvle2  38248  hsphoidmvle  38249  hoidmv1lelem2  38255  hoidmvle  38263  ovnhoilem1  38264  bgoldbtbndlem2  38708  bgoldbtbndlem3  38709  bgoldbtbndlem4  38710  bgoldbtbnd  38711  fsummsndifre  38859  fsummmodsndifre  38861  usgruspgrb  39018  nbumgrvtx  39144  nbupgrres  39168  isuvtxa  39191  cusgrexi  39229  cusgrres  39231  cusgrfilem2  39239  c0rhm  39497  c0rnghm  39498  zrrnghm  39502  2zrngnmlid2  39536  zrinitorngc  39587  zrtermorngc  39588  mgpsumunsn  39730  mgpsumz  39731  mgpsumn  39732  lindslinindsimp1  39837  lindslinindsimp2  39843  lincresunit1  39857  lincresunit2  39858  lincresunit3lem1  39859  lincresunit3lem2  39860  lincresunit3  39861  lindssnlvec  39866  logcxp0  39933  relogbmulbexp  39959  relogbdivb  39960  dignn0fr  39999
  Copyright terms: Public domain W3C validator