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

Theorem eldifi 3473
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 3333 . 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 1756    \ cdif 3320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-dif 3326
This theorem is referenced by:  difss  3478  noel  3636  tz7.7  4740  tfi  6459  peano5  6494  tz7.48-1  6890  tz7.49  6892  dif20el  6937  oaf1o  6994  oeordi  7018  oeord  7019  oecan  7020  oeword  7021  oeworde  7024  oelimcl  7031  oeeulem  7032  oeeui  7033  oaabs2  7076  boxcutc  7298  domdifsn  7386  isinf  7518  pssnn  7523  pwfilem  7597  fsuppco2  7644  fsuppcor  7645  ordtypelem7  7730  unxpwdom2  7795  inf3lem3  7828  cantnfp1lem1  7878  cantnfp1lem3  7880  cantnfp1lem1OLD  7904  cantnfp1lem3OLD  7906  infxpenc2lem1  8177  dfacacn  8302  isf32lem3  8516  isf34lem4  8538  fin67  8556  isfin7-2  8557  domtriomlem  8603  axdc2lem  8609  axdc3lem4  8614  axdc4lem  8616  ttukeylem7  8676  konigthlem  8724  fpwwe2lem13  8801  fpwwe2  8802  hashf1lem1  12200  rlimrege0  13049  rlimrecl  13050  sumrblem  13180  fsumcvg  13181  summolem2a  13184  fsumss  13194  fsumless  13251  cvgcmpce  13273  binomlem  13284  incexclem  13291  incexc  13292  isumltss  13303  rpnnen2lem10  13498  rpnnen2lem11  13499  oddprm  13874  iserodd  13894  prmreclem2  13970  prmreclem3  13971  prmreclem5  13973  4sqlem19  14016  prmlem0  14125  firest  14363  grpinvnzcl  15589  symgextfv  15914  pmtrf  15952  pmtrdifellem3  15975  sylow2alem2  16108  sylow2a  16109  efgsf  16217  efgsrel  16222  efgs1  16223  efgsfo  16227  efgredlemc  16233  gsumzaddlem  16399  gsumzadd  16400  gsumzaddlemOLD  16401  gsumzaddOLD  16402  gsumzmhm  16420  gsumzmhmOLD  16421  gsumzinvOLD  16433  gsumsubOLD  16438  gsum2d2lem  16455  dprdfadd  16500  dprdfaddOLD  16507  dprdres  16515  subgdmdprd  16521  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  dmdprdsplit2lem  16534  dpjidcl  16547  dpjidclOLD  16554  ablfac1b  16561  pgpfac1lem1  16565  gsummgp0  16689  isirred  16781  irredrmul  16789  isdrng2  16822  isdrngd  16837  lcomfsupOLD  16964  lcomfsupp  16965  lbspropd  17160  lspsneq  17183  lsppratlem6  17213  lbsextlem2  17220  lbsextlem4  17222  rngelnzr  17327  psrbaglesupp  17415  psrbaglesuppOLD  17416  psrlidm  17454  psrlidmOLD  17455  psrridm  17456  psrridmOLD  17457  mplsubglem  17490  mpllsslem  17491  mplsubglemOLD  17492  mpllsslemOLD  17493  mplsubrglem  17497  mplsubrglemOLD  17498  mplmonmul  17523  mplcoe1  17524  mplcoe5  17528  mplcoe2OLD  17530  mplbas2  17531  mplbas2OLD  17532  evlslem3  17580  coe1tmmul2  17709  coe1tmmul  17710  xrs1mnd  17831  xrs10  17832  xrs1cmn  17833  cnsubrg  17853  psgnodpm  17998  zrhpsgnodpm  18002  evpmodpmf1o  18006  uvcresum  18198  frlmssuvc1  18199  frlmssuvc1OLD  18201  frlmsslsp  18203  frlmsslspOLD  18204  frlmup2  18207  lindfrn  18230  f1lindf  18231  lindfmm  18236  islindf4  18247  1marepvsma1  18374  mdet1  18388  mdetrlin  18389  mdetrsca  18390  mdetralt  18394  maducoeval2  18426  madugsum  18429  symgmatr01  18440  gsummatr01lem3  18443  gsummatr01lem4  18444  gsummatr01  18445  smadiadetlem0  18447  smadiadetlem1a  18449  cmpfi  18991  2ndcdisj2  19041  elptr2  19127  ptcnplem  19174  xkopt  19208  kqdisj  19285  fin1aufil  19485  ptcmplem2  19605  ptcmplem3  19606  ptcmplem4  19607  opnsubg  19658  lpbl  20058  blcld  20060  zcld  20370  recld2  20371  reconnlem1  20383  divcn  20424  iundisj  21009  mbfeqalem  21100  itg1val2  21142  itg1ge0  21144  i1fmullem  21152  i1fadd  21153  itg1addlem4  21157  itg1mulc  21162  itg1lea  21170  itg1le  21171  mbfi1fseqlem4  21176  itg2uba  21201  itg2lea  21202  itg2eqa  21203  itg2splitlem  21206  itg2split  21207  itgeqa  21271  ellimc3  21334  dvaddbr  21392  dvmulbr  21393  dvcobr  21400  dvcjbr  21403  dvrec  21409  dvcnvlem  21428  dvexp3  21430  dveflem  21431  tdeglem4  21509  deg1n0ima  21540  deg1mul3le  21568  ig1peu  21623  ply1termlem  21651  plypf1  21660  plyaddlem1  21661  plymullem1  21662  coeeulem  21672  coeidlem  21685  coeid3  21688  coefv0  21695  coemulhi  21701  coemulc  21702  dvply1  21730  fta1  21754  vieta1lem2  21757  elaa  21762  elqaalem2  21766  aannenlem2  21775  aaliou2  21786  tayl0  21807  dvtaylp  21815  taylthlem1  21818  taylthlem2  21819  pserdvlem2  21873  dcubic  22221  rlimcnp  22339  jensen  22362  wilthlem2  22387  basellem3  22400  chpub  22539  logexprlim  22544  lgslem1  22615  lgslem4  22618  lgsvalmod  22634  lgsqr  22665  lgsquadlem1  22673  lgsquad2  22679  m1lgs  22681  dchrisum0fno1  22740  rplogsum  22756  cusgraexi  23344  uvtxnbgra  23369  cusconngra  23530  ablomul  23810  mulid  23811  zerdivemp1  23889  strlem1  25622  strlem3  25625  strlem4  25626  strlem5  25627  hstrlem3  25633  hstrlem4  25634  iundisjf  25899  iundisjfi  26048  elzdif0  26378  logbcl  26425  ind0  26445  measvunilem  26595  eulerpartlemb  26720  eulerpartlemf  26722  sseqf  26744  ballotlem5  26851  ballotlemi1  26854  ballotlemii  26855  ballotlemic  26858  ballotlem1c  26859  ballotlemscr  26870  ballotlemro  26874  ballotlemfg  26877  ballotlemfrc  26878  ballotlemfrceq  26880  ballotlemrinv0  26884  plymulx0  26917  signstfvn  26939  dmgmaddn0  26978  dmlogdmgm  26979  lgamgulmlem2  26985  igamz  27003  gamp1  27013  regamcl  27016  subfacp1lem1  27036  circum  27288  prodrblem  27411  fprodcvg  27412  prodmolem2a  27416  fprodss  27430  dfon2lem6  27570  wfrlem10  27702  wfrlem15  27707  dvtan  28413  itg2addnclem2  28415  ftc1cnnc  28437  dvasin  28451  dvreasin  28453  dvreacos  28454  neibastop1  28551  isdrngo2  28735  isdrngo3  28736  divrngidl  28799  isfldidl  28839  pridlc2  28843  pridlc3  28844  prter2  28997  irrapx1  29140  pell1234qrne0  29165  pell1234qrreccl  29166  pell1234qrmulcl  29167  pell14qrgt0  29171  pell1234qrdich  29173  pell14qrdich  29181  pell1qrge1  29182  pell1qr1  29183  pell1qrgap  29186  pell14qrgapw  29188  pellqrexplicit  29189  pellqrex  29191  pellfundge  29194  pellfundgt1  29195  setindtr  29344  kelac1  29387  mpaaeu  29478  flcidc  29502  cntzsdrg  29530  deg1mhm  29546  climrec  29747  stoweidlem25  29791  stoweidlem28  29794  stoweidlem41  29807  stoweidlem44  29810  stoweidlem46  29812  stirlinglem5  29844  fsummsndifre  30208  fsummmodsndifre  30210  frgrancvvdeqlem9  30605  frgrancvvdeq  30606  frgrancvvdgeq  30607  2spotiundisj  30626  frghash2spot  30627  mgpsumunsn  30728  mgpsumz  30729  mgpsumn  30730  dmatmul  30836  mdetdiaglem  30866  lindslinindsimp1  30922  lindslinindsimp2  30928  lincresunit1  30942  lincresunit2  30943  lincresunit3lem1  30944  lincresunit3lem2  30945  lincresunit3  30946  lindssnlvec  30951  elogb  31041  bnj923  31690  bnj570  31827  bnj594  31834  lsateln0  32533  lsatlss  32534  lsmsat  32546  lsatcv0  32569  lsat0cv  32571  lcv1  32579  l1cvpat  32592  dih1dimatlem  34867  dihatexv2  34877  djhcvat42  34953  dihjat1lem  34966  dochsatshp  34989  lcfl6  35038  mapdrvallem2  35183  mapdpglem32  35243  mapdh9aOLDN  35329  hdmap1eulemOLDN  35363
  Copyright terms: Public domain W3C validator