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

Theorem eldifi 3567
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 3426 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 466 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1898    \ cdif 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-dif 3419
This theorem is referenced by:  difss  3572  noel  3747  eqoreldif  4025  xpdifid  5284  tz7.7  5468  tfi  6707  peano5  6743  wfrlem10  7071  wfrlem15  7076  tz7.48-1  7186  tz7.49  7188  dif20el  7233  oaf1o  7290  oeordi  7314  oeord  7315  oecan  7316  oeword  7317  oeworde  7320  oelimcl  7327  oeeulem  7328  oeeui  7329  oaabs2  7372  boxcutc  7591  domdifsn  7681  isinf  7811  pssnn  7816  pwfilem  7894  fsuppco2  7942  fsuppcor  7943  ordtypelem7  8065  unxpwdom2  8129  inf3lem3  8161  cantnfp1lem1  8209  cantnfp1lem3  8211  infxpenc2lem1  8476  dfacacn  8597  isf32lem3  8811  isf34lem4  8833  fin67  8851  isfin7-2  8852  domtriomlem  8898  axdc2lem  8904  axdc3lem4  8909  axdc4lem  8911  ttukeylem7  8971  konigthlem  9019  fpwwe2lem13  9093  fpwwe2  9094  hashf1lem1  12651  rlimrege0  13692  rlimrecl  13693  sumrblem  13826  fsumcvg  13827  summolem2a  13830  fsumss  13840  fsumless  13905  cvgcmpce  13927  binomlem  13936  incexclem  13943  incexc  13944  isumltss  13955  prodrblem  14032  fprodcvg  14033  prodmolem2a  14037  fprodss  14051  fprodn0f  14094  fprodeq0g  14097  rpnnen2lem10  14325  rpnnen2lem11  14326  fproddvdsd  14419  lcmfunsnlem2  14662  oddprm  14814  iserodd  14834  prmreclem2  14910  prmreclem3  14911  prmreclem5  14913  4sqlem19  14962  prmdvdsprmo  15049  prmodvdslcmf  15054  prmdvdsprmorOLD  15064  prmordvdslcmfOLD  15068  prmordvdslcmsOLDOLD  15070  prmlem0  15126  firest  15380  grpinvnzcl  16775  symgextfv  17108  pmtrf  17145  pmtrdifellem3  17168  sylow2alem2  17319  sylow2a  17320  efgsf  17428  efgsrel  17433  efgs1  17434  efgsfo  17438  efgredlemc  17444  gsumzaddlem  17603  gsumzadd  17604  gsumzmhm  17619  gsum2d2lem  17654  dprdfadd  17702  dprdres  17710  subgdmdprd  17716  dmdprdsplitlem  17719  dmdprdsplit2lem  17727  dpjidcl  17740  ablfac1b  17752  pgpfac1lem1  17756  gsummgp0  17885  isirred  17976  irredrmul  17984  isdrng2  18034  isdrngd  18049  lcomfsupp  18177  lbspropd  18371  lspsneq  18394  lsppratlem6  18424  lbsextlem2  18431  lbsextlem4  18433  ringelnzr  18539  psrbaglesupp  18641  psrlidm  18676  psrridm  18677  mplsubglem  18707  mpllsslem  18708  mplsubrglem  18712  mplmonmul  18737  mplcoe1  18738  mplcoe5  18741  mplbas2  18743  evlslem3  18786  coe1tmmul2  18918  coe1tmmul  18919  xrs1mnd  19055  xrs10  19056  xrs1cmn  19057  cnsubrg  19077  psgnodpm  19205  zrhpsgnodpm  19209  evpmodpmf1o  19213  uvcresum  19400  frlmssuvc1  19401  frlmsslsp  19403  frlmup2  19406  lindfrn  19428  f1lindf  19429  lindfmm  19434  islindf4  19445  dmatmul  19571  1marepvsma1  19657  mdetdiaglem  19672  mdetrlin  19676  mdetrsca  19677  mdetralt  19682  maducoeval2  19714  madugsum  19717  symgmatr01  19728  gsummatr01lem3  19731  gsummatr01lem4  19732  gsummatr01  19733  smadiadetlem0  19735  smadiadetlem1a  19737  cmpfi  20472  2ndcdisj2  20521  elptr2  20638  ptcnplem  20685  xkopt  20719  kqdisj  20796  fin1aufil  20996  ptcmplem2  21117  ptcmplem3  21118  ptcmplem4  21119  opnsubg  21171  lpbl  21567  blcld  21569  zcld  21880  recld2  21881  reconnlem1  21893  divcn  21949  iundisj  22550  mbfeqalem  22647  itg1val2  22691  itg1ge0  22693  i1fmullem  22701  i1fadd  22702  itg1addlem4  22706  itg1mulc  22711  itg1lea  22719  itg1le  22720  mbfi1fseqlem4  22725  itg2uba  22750  itg2lea  22751  itg2eqa  22752  itg2splitlem  22755  itg2split  22756  itgeqa  22820  ellimc3  22883  dvaddbr  22941  dvmulbr  22942  dvcobr  22949  dvcjbr  22952  dvrec  22958  dvcnvlem  22977  dvexp3  22979  dveflem  22980  tdeglem4  23058  deg1n0ima  23087  deg1mul3le  23114  ig1peu  23171  ig1peuOLD  23172  ply1termlem  23206  plypf1  23215  plyaddlem1  23216  plymullem1  23217  coeeulem  23227  coeidlem  23240  coeid3  23243  coefv0  23251  coemulhi  23257  coemulc  23258  dvply1  23286  fta1  23310  vieta1lem2  23313  elaa  23318  elqaalem2  23322  elqaalem2OLD  23325  aannenlem2  23334  aaliou2  23345  tayl0  23366  dvtaylp  23374  taylthlem1  23377  taylthlem2  23378  pserdvlem2  23432  logbcl  23753  relogbreexp  23761  relogbcxp  23771  cxplogb  23772  dcubic  23821  rlimcnp  23940  jensen  23963  dmgmaddn0  23997  dmlogdmgm  23998  lgamgulmlem2  24004  igamz  24022  gamp1  24032  regamcl  24035  wilthlem2  24043  basellem3  24058  chpub  24197  logexprlim  24202  lgslem1  24273  lgslem4  24276  lgsvalmod  24292  lgsqr  24323  lgsquadlem1  24331  lgsquad2  24337  m1lgs  24339  dchrisum0fno1  24398  rplogsum  24414  ishpg  24850  cusgraexi  25245  uvtxnbgra  25270  cusconngra  25453  frgrancvvdeqlem9  25818  frgrancvvdeq  25819  frgrancvvdgeq  25820  2spotiundisj  25839  frghash2spot  25840  ablomul  26132  mulid  26133  zerdivemp1  26211  strlem1  27952  strlem3  27955  strlem4  27956  strlem5  27957  hstrlem3  27963  hstrlem4  27964  iundisjf  28248  suppss3  28361  iundisjfi  28421  qtophaus  28712  elzdif0  28833  ind0  28890  measvunilem  29083  sibfof  29222  eulerpartlemb  29250  eulerpartlemf  29252  sseqf  29274  ballotlem5  29381  ballotlemi1  29384  ballotlemii  29385  ballotlemic  29388  ballotlem1c  29389  ballotlemscr  29400  ballotlemro  29404  ballotlemfg  29407  ballotlemfrc  29408  ballotlemfrceq  29410  ballotlemrinv0  29414  ballotlemi1OLD  29422  ballotlemiiOLD  29423  ballotlemicOLD  29426  ballotlem1cOLD  29427  ballotlemscrOLD  29438  ballotlemroOLD  29442  ballotlemfgOLD  29445  ballotlemfrcOLD  29446  ballotlemfrceqOLD  29448  ballotlemrinv0OLD  29452  plymulx0  29485  signstfvn  29507  bnj923  29628  bnj570  29765  bnj594  29772  subfacp1lem1  29951  mrsubcn  30206  mrsubco  30208  circum  30367  dfon2lem6  30483  neibastop1  31064  poimirlem24  32009  poimirlem25  32010  dvtan  32037  itg2addnclem2  32039  ftc1cnnc  32061  dvasin  32073  dvreasin  32075  dvreacos  32076  isdrngo2  32242  isdrngo3  32243  divrngidl  32306  isfldidl  32346  pridlc2  32350  pridlc3  32351  prter2  32498  lsateln0  32606  lsatlss  32607  lsmsat  32619  lsatcv0  32642  lsat0cv  32644  lcv1  32652  l1cvpat  32665  dih1dimatlem  34942  dihatexv2  34952  djhcvat42  35028  dihjat1lem  35041  dochsatshp  35064  lcfl6  35113  mapdrvallem2  35258  mapdpglem32  35318  irrapx1  35717  pell1234qrne0  35744  pell1234qrreccl  35745  pell1234qrmulcl  35746  pell14qrgt0  35750  pell1234qrdich  35752  pell14qrdich  35760  pell1qrge1  35761  pell1qr1  35762  pell1qrgap  35765  pell14qrgapw  35767  pellqrexplicit  35768  pellqrex  35771  pellfundge  35775  pellfundgt1  35776  setindtr  35924  kelac1  35966  mpaaeu  36061  flcidc  36085  cntzsdrg  36113  deg1mhm  36129  radcnvrat  36707  binomcxplemdvbinom  36746  disjiun2  37436  fiiuncl  37444  disjf1o  37504  icoiccdif  37663  iccdificc  37679  fsumnncl  37688  fsumsplit1  37689  fsumsupp0  37695  fprod0  37714  climrec  37719  islpcn  37757  lptre2pt  37758  limclner  37770  fprodcncf  37817  dvrecg  37820  fperdvper  37828  dvdivcncf  37837  dvnmul  37856  dvmptfprodlem  37857  dvnprodlem2  37860  stoweidlem25  37923  stoweidlem28  37926  stoweidlem41  37940  stoweidlem44  37943  stoweidlem46  37945  stirlinglem5  37978  dirkercncflem1  38003  dirkercncflem2  38004  fourierdlem24  38031  fourierdlem62  38070  fouriersw  38133  fouriercn  38134  elaa2lem  38135  elaa2lemOLD  38136  elaa2  38137  etransclem25  38162  etransclem35  38172  etransclem44  38181  sge0iunmptlemfi  38293  sge0fodjrnlem  38296  iundjiunlem  38335  meadjiunlem  38341  isomenndlem  38389  hsphoidmvle2  38445  hsphoidmvle  38446  hoidmv1lelem2  38452  hoidmvle  38460  ovnhoilem1  38461  hspdifhsp  38476  hspmbllem2  38487  bgoldbtbndlem2  38939  bgoldbtbndlem3  38940  bgoldbtbndlem4  38941  bgoldbtbnd  38942  fsummsndifre  39137  fsummmodsndifre  39139  usgruspgrb  39316  nbumgrvtx  39464  nbupgrres  39488  isuvtxa  39517  cusgrexi  39557  cusgrres  39559  cusgrfilem2  39567  umgrislfupgrlem  39718  cusconngr  39932  c0rhm  40185  c0rnghm  40186  zrrnghm  40190  2zrngnmlid2  40224  zrinitorngc  40275  zrtermorngc  40276  mgpsumunsn  40416  mgpsumz  40417  mgpsumn  40418  lindslinindsimp1  40523  lindslinindsimp2  40529  lincresunit1  40543  lincresunit2  40544  lincresunit3lem1  40545  lincresunit3lem2  40546  lincresunit3  40547  lindssnlvec  40552  logcxp0  40619  relogbmulbexp  40645  relogbdivb  40646  dignn0fr  40685
  Copyright terms: Public domain W3C validator