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

Theorem eldifi 3437
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 3298 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 447 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1721    \ cdif 3285
This theorem is referenced by:  difss  3442  noel  3600  tz7.7  4575  tfi  4800  peano5  4835  tz7.48-1  6667  tz7.49  6669  dif20el  6716  oaf1o  6773  oeordi  6797  oeord  6798  oecan  6799  oeword  6800  oeworde  6803  oelimcl  6810  oeeulem  6811  oeeui  6812  oaabs2  6855  boxcutc  7072  domdifsn  7158  isinf  7289  pssnn  7294  pwfilem  7367  ordtypelem7  7457  unxpwdom2  7520  inf3lem3  7549  cantnfp1lem1  7598  cantnfp1lem3  7600  infxpenc2lem1  7864  dfacacn  7985  isf32lem3  8199  isf34lem4  8221  fin67  8239  isfin7-2  8240  domtriomlem  8286  axdc2lem  8292  axdc3lem4  8297  axdc4lem  8299  ttukeylem7  8359  konigthlem  8407  fpwwe2lem13  8481  fpwwe2  8482  hashf1lem1  11667  rlimrege0  12336  rlimrecl  12337  sumrblem  12468  fsumcvg  12469  summolem2a  12472  fsumss  12482  fsumless  12538  cvgcmpce  12560  binomlem  12571  incexclem  12579  incexc  12580  isumltss  12591  rpnnen2lem10  12786  rpnnen2lem11  12787  oddprm  13152  iserodd  13172  prmreclem2  13248  prmreclem3  13249  prmreclem5  13251  4sqlem19  13294  prmlem0  13391  firest  13623  grpinvnzcl  14826  sylow2alem2  15215  sylow2a  15216  efgsf  15324  efgsrel  15329  efgs1  15330  efgsfo  15334  efgredlemc  15340  gsumzaddlem  15489  gsumzadd  15490  gsumzmhm  15496  gsumzinv  15503  gsumsub  15505  gsum2d2lem  15510  dprdfadd  15541  dprdsubg  15545  dprdres  15549  subgdmdprd  15555  dmdprdsplitlem  15558  dmdprdsplit2lem  15566  dpjidcl  15579  ablfac1b  15591  pgpfac1lem1  15595  isirred  15767  irredrmul  15775  isdrng2  15808  isdrngd  15823  lbspropd  16134  lspsneq  16157  lsppratlem6  16187  lbsextlem2  16194  lbsextlem4  16196  rngelnzr  16299  psrbaglesupp  16396  psrlidm  16430  psrridm  16431  mplsubglem  16461  mpllsslem  16462  mplsubrglem  16465  mplmonmul  16490  mplcoe1  16491  mplcoe2  16493  mplbas2  16494  coe1tmmul2  16631  coe1tmmul  16632  xrs1mnd  16699  xrs10  16700  xrs1cmn  16701  cnsubrg  16722  cmpfi  17433  2ndcdisj2  17481  elptr2  17567  ptcnplem  17614  xkopt  17648  kqdisj  17725  fin1aufil  17925  ptcmplem2  18045  ptcmplem3  18046  ptcmplem4  18047  opnsubg  18098  lpbl  18494  blcld  18496  zcld  18805  recld2  18806  reconnlem1  18818  divcn  18859  iundisj  19403  mbfeqalem  19495  itg1val2  19537  itg1ge0  19539  i1fmullem  19547  i1fadd  19548  itg1addlem4  19552  itg1mulc  19557  itg1lea  19565  itg1le  19566  mbfi1fseqlem4  19571  itg2uba  19596  itg2lea  19597  itg2eqa  19598  itg2splitlem  19601  itg2split  19602  itgeqa  19666  ellimc3  19727  dvaddbr  19785  dvmulbr  19786  dvcobr  19793  dvcjbr  19796  dvrec  19802  dvcnvlem  19821  dvexp3  19823  dveflem  19824  evlslem3  19896  tdeglem4  19944  mdeg0  19954  deg1n0ima  19973  deg1mul3le  20000  ig1peu  20055  ply1termlem  20083  plypf1  20092  plyaddlem1  20093  plymullem1  20094  coeeulem  20104  coeidlem  20117  coeid3  20120  coefv0  20127  coemulhi  20133  coemulc  20134  dvply1  20162  fta1  20186  vieta1lem2  20189  elaa  20194  elqaalem2  20198  aannenlem2  20207  aaliou2  20218  tayl0  20239  dvtaylp  20247  taylthlem1  20250  taylthlem2  20251  pserdvlem2  20305  dcubic  20647  rlimcnp  20765  jensen  20788  wilthlem2  20813  basellem3  20826  chpub  20965  logexprlim  20970  lgslem1  21041  lgslem4  21044  lgsvalmod  21060  lgsqr  21091  lgsquadlem1  21099  lgsquad2  21105  m1lgs  21107  dchrisum0fno1  21166  rplogsum  21182  cusgraexi  21438  uvtxnbgra  21463  cusconngra  21624  ablomul  21904  mulid  21905  zerdivemp1  21983  strlem1  23714  strlem3  23717  strlem4  23718  strlem5  23719  hstrlem3  23725  hstrlem4  23726  iundisjf  23990  iundisjfi  24113  elzdif0  24325  logbcl  24358  ind0  24378  measvunilem  24527  ballotlem5  24718  ballotlemi1  24721  ballotlemii  24722  ballotlemic  24725  ballotlem1c  24726  ballotlemscr  24737  ballotlemro  24741  ballotlemfg  24744  ballotlemfrc  24745  ballotlemfrceq  24747  ballotlemrinv0  24751  dmgmaddn0  24768  dmlogdmgm  24769  lgamgulmlem2  24775  igamz  24793  gamp1  24803  regamcl  24806  subfacp1lem1  24826  circum  25072  prodrblem  25216  fprodcvg  25217  prodmolem2a  25221  fprodss  25235  dfon2lem6  25366  wfrlem10  25487  wfrlem15  25492  itg2addnclem2  26164  ftc1cnnc  26186  dvreasin  26187  neibastop1  26286  isdrngo2  26472  isdrngo3  26473  divrngidl  26536  isfldidl  26576  pridlc2  26580  pridlc3  26581  prter2  26628  lcomfsup  26645  irrapx1  26789  pell1234qrne0  26814  pell1234qrreccl  26815  pell1234qrmulcl  26816  pell14qrgt0  26820  pell1234qrdich  26822  pell14qrdich  26830  pell1qrge1  26831  pell1qr1  26832  pell1qrgap  26835  pell14qrgapw  26837  pellqrexplicit  26838  pellqrex  26840  pellfundge  26843  pellfundgt1  26844  setindtr  26993  kelac1  27037  uvcresum  27118  frlmssuvc1  27122  frlmsslsp  27124  frlmup1  27126  frlmup2  27127  lindfrn  27167  f1lindf  27168  lindfmm  27173  islindf4  27184  mpaaeu  27231  flcidc  27255  pmtrf  27273  mamulid  27334  mamurid  27335  cntzsdrg  27386  deg1mhm  27402  climrec  27604  stoweidlem25  27649  stoweidlem28  27652  stoweidlem41  27665  stoweidlem44  27668  stoweidlem46  27670  stirlinglem5  27702  frgrancvvdeqlem9  28152  frgrancvvdeq  28153  frgrancvvdgeq  28154  2spotiundisj  28173  frghash2spot  28174  elogb  28254  bnj923  28855  bnj570  28994  bnj594  29001  lsateln0  29490  lsatlss  29491  lsmsat  29503  lsatcv0  29526  lsat0cv  29528  lcv1  29536  l1cvpat  29549  dih1dimatlem  31824  dihatexv2  31834  djhcvat42  31910  dihjat1lem  31923  dochsatshp  31946  lcfl6  31995  mapdrvallem2  32140  mapdpglem32  32200  mapdh9aOLDN  32286  hdmap1eulemOLDN  32320
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-dif 3291
  Copyright terms: Public domain W3C validator