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

Theorem eldifi 3298
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 3162 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 446 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1684    \ cdif 3149
This theorem is referenced by:  difss  3303  noel  3459  tz7.7  4418  tfi  4644  peano5  4679  tz7.48-1  6455  tz7.49  6457  dif20el  6504  oaf1o  6561  oeordi  6585  oeord  6586  oecan  6587  oeword  6588  oeworde  6591  oelimcl  6598  oeeulem  6599  oeeui  6600  oaabs2  6643  boxcutc  6859  domdifsn  6945  isinf  7076  pssnn  7081  unblem1  7109  pwfilem  7150  ordtypelem7  7239  unxpwdom2  7302  inf3lem3  7331  cantnfp1lem1  7380  cantnfp1lem3  7382  cantnflem3  7393  cantnflem4  7394  oef1o  7401  infxpenc  7645  infxpenc2lem1  7646  dfacacn  7767  infpssrlem3  7931  isf32lem3  7981  isf34lem4  8003  fin67  8021  isfin7-2  8022  domtriomlem  8068  axdc2lem  8074  axdc3lem4  8079  axdc4lem  8081  ttukeylem7  8142  konigthlem  8190  fpwwe2lem13  8264  fpwwe2  8265  pwfseqlem4a  8283  expclz  11128  hashf1lem1  11393  rlimrege0  12053  rlimrecl  12054  sumrblem  12184  fsumcvg  12185  summolem2a  12188  fsumss  12198  fsumless  12254  cvgcmpce  12276  binomlem  12287  incexclem  12295  incexc  12296  isumltss  12307  rpnnen2lem10  12502  rpnnen2lem11  12503  oddprm  12868  iserodd  12888  prmreclem2  12964  prmreclem3  12965  prmreclem5  12967  4sqlem19  13010  prmlem0  13107  firest  13337  grpinvnzcl  14540  sylow2alem2  14929  sylow2a  14930  efgsf  15038  efgsdmi  15041  efgsrel  15043  efgs1  15044  efgs1b  15045  efgsp1  15046  efgsres  15047  efgsfo  15048  efgredlemf  15050  efgredlemd  15053  efgredlemc  15054  efgredlem  15056  efgrelexlemb  15059  gsumzaddlem  15203  gsumzadd  15204  gsumzmhm  15210  gsumzinv  15217  gsumsub  15219  gsum2d2lem  15224  dprdfadd  15255  dprdsubg  15259  dprdres  15263  subgdmdprd  15269  dmdprdsplitlem  15272  dmdprdsplit2lem  15280  dpjidcl  15293  ablfac1b  15305  pgpfac1lem1  15309  pgpfac1lem2  15310  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfac1lem4  15313  isirred  15481  irredrmul  15489  isdrng2  15522  isdrngd  15537  lbspropd  15852  lvecinv  15866  lspsncmp  15869  lspsnne1  15870  lspsnnecom  15872  lspabs2  15873  lspsneq  15875  lspsneu  15876  lspdisjb  15879  lspexch  15882  lspindp1  15886  lvecindp2  15892  lspsolv  15896  lspsnat  15898  lsppratlem6  15905  lbsextlem2  15912  lbsextlem4  15914  rngelnzr  16017  fidomndrnglem  16047  psrbaglesupp  16114  psrlidm  16148  psrridm  16149  mplsubglem  16179  mpllsslem  16180  mplsubrglem  16183  mplmonmul  16208  mplcoe1  16209  mplcoe2  16211  mplbas2  16212  coe1tmmul2  16352  coe1tmmul  16353  xrs1mnd  16409  xrs10  16410  xrs1cmn  16411  cnsubrg  16432  cmpfi  17135  2ndcdisj2  17183  1stccnp  17188  elptr2  17269  ptcnplem  17315  xkopt  17349  kqdisj  17423  fin1aufil  17627  ptcmplem2  17747  ptcmplem3  17748  ptcmplem4  17749  opnsubg  17790  lpbl  18049  blcld  18051  zcld  18319  recld2  18320  reconnlem1  18331  divcn  18372  iundisj  18905  mbfeqalem  18997  itg1val2  19039  itg1ge0  19041  i1fmullem  19049  i1fadd  19050  itg1addlem4  19054  itg1mulc  19059  itg1lea  19067  itg1le  19068  mbfi1fseqlem4  19073  itg2uba  19098  itg2lea  19099  itg2eqa  19100  itg2splitlem  19103  itg2split  19104  itgeqa  19168  ellimc3  19229  dvaddbr  19287  dvmulbr  19288  dvcobr  19295  dvcjbr  19298  dvrec  19304  dvcnvlem  19323  dvexp3  19325  dveflem  19326  ftc1lem6  19388  evlslem3  19398  tdeglem4  19446  mdeg0  19456  deg1n0ima  19475  deg1mul3le  19502  ig1peu  19557  ply1termlem  19585  plypf1  19594  plyaddlem1  19595  plymullem1  19596  coeeulem  19606  coeidlem  19619  coeid3  19622  coefv0  19629  coemulhi  19635  coemulc  19636  dvply1  19664  fta1  19688  vieta1lem2  19691  elaa  19696  elqaalem1  19699  elqaalem2  19700  aannenlem2  19709  aaliou2  19720  tayl0  19741  dvtaylp  19749  taylthlem1  19752  taylthlem2  19753  ulmdvlem3  19779  pserdvlem2  19804  abelthlem6  19812  abelthlem7a  19813  abelthlem7  19814  logtayl  20007  dcubic  20142  rlimcnp  20260  jensen  20283  wilthlem2  20307  basellem3  20320  chpub  20459  logexprlim  20464  lgslem1  20535  lgslem4  20538  lgsvalmod  20554  lgsqrlem1  20580  lgsqrlem2  20581  lgsqrlem3  20582  lgsqrlem4  20583  lgsqr  20585  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem3  20590  lgseisenlem4  20591  lgseisen  20592  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  lgsquad2  20599  m1lgs  20601  dchrisum0fno1  20660  dchrisum0re  20662  dchrisum0lema  20663  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  rplogsum  20676  ablomul  21022  mulid  21023  strlem1  22830  strlem3  22833  strlem4  22834  strlem5  22835  hstrlem3  22841  hstrlem4  22842  ballotlemi1  23061  ballotlemii  23062  ballotlemic  23065  ballotlem1c  23066  ballotlemscr  23077  ballotlemro  23081  ballotlemfg  23084  ballotlemfrc  23085  ballotlemfrceq  23087  ballotlemrinv0  23091  iundisjfi  23363  iundisjf  23365  logbcl  23399  measvuni  23542  ind0  23603  dmgmaddn0  23695  dmgmseqn0  23696  subfacp1lem1  23710  circum  24007  dfon2lem6  24144  wfrlem10  24265  wfrlem15  24270  dvreasin  24923  zerdivemp1  25436  bsstr  26128  nbssntr  26129  lppotos  26144  bsstrs  26146  nbssntrs  26147  bosser  26167  pdiveql  26168  neibastop1  26308  rrndstprj2  26555  isdrngo2  26589  isdrngo3  26590  divrngidl  26653  isfldidl  26693  pridlc2  26697  pridlc3  26698  prter2  26749  lcomfsup  26768  irrapx1  26913  pell1234qrne0  26938  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell14qrgt0  26944  pell1234qrdich  26946  pell14qrdich  26954  pell1qrge1  26955  pell1qr1  26956  pell1qrgap  26959  pell14qrgapw  26961  pellqrexplicit  26962  pellqrex  26964  pellfundge  26967  pellfundgt1  26968  qirropth  26993  rmxyneg  27005  rmxm1  27019  rmxluc  27021  rmxdbl  27024  ltrmxnn0  27036  jm2.19lem1  27082  jm2.23  27089  rmxdiophlem  27108  setindtr  27117  aomclem2  27152  kelac1  27161  uvcresum  27242  frlmssuvc1  27246  frlmssuvc2  27247  frlmsslsp  27248  frlmup1  27250  frlmup2  27251  lindfrn  27291  f1lindf  27292  lindfmm  27297  islindf4  27308  mpaaeu  27355  flcidc  27379  pmtrf  27397  symggen  27411  mamulid  27458  mamurid  27459  cntzsdrg  27510  deg1mhm  27526  climrec  27729  stoweidlem25  27774  stoweidlem28  27777  stoweidlem34  27783  stoweidlem41  27790  stoweidlem43  27792  stoweidlem44  27793  stoweidlem46  27795  stirlinglem5  27827  uvtxnbgra  28165  bnj923  28798  bnj570  28937  bnj594  28944  lsateln0  29185  lsatlss  29186  lsmsat  29198  lsatfixedN  29199  lsatcv0  29221  lsat0cv  29223  lcv1  29231  l1cvpat  29244  lkreqN  29360  lkrlspeqN  29361  dih1dimatlem  31519  dihatexv2  31529  dochnel2  31582  dochnel  31583  djhcvat42  31605  dihjat1lem  31618  dochsatshp  31641  dochsnshp  31643  dochexmidat  31649  dochsnkr  31662  dochsnkr2  31663  dochsnkr2cl  31664  dochflcl  31665  dochfl1  31666  dochfln0  31667  lcfl6lem  31688  lcfl7lem  31689  lcfl6  31690  lcfl8b  31694  lclkrlem2a  31697  lclkrlem2b  31698  lclkrlem2c  31699  lclkrlem2d  31700  lclkrlem2e  31701  lclkrlem2f  31702  lcfrlem14  31746  lcfrlem15  31747  lcfrlem16  31748  lcfrlem17  31749  lcfrlem18  31750  lcfrlem19  31751  lcfrlem20  31752  lcfrlem21  31753  lcfrlem23  31755  lcfrlem25  31757  lcfrlem26  31758  lcfrlem35  31767  lcfrlem36  31768  mapdrvallem2  31835  mapdn0  31859  mapdpglem29  31890  mapdpglem24  31894  mapdpglem32  31895  baerlem3lem1  31897  baerlem5alem1  31898  baerlem5blem1  31899  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  baerlem5amN  31906  baerlem5bmN  31907  baerlem5abmN  31908  mapdindp0  31909  mapdindp1  31910  mapdindp2  31911  mapdindp3  31912  mapdindp4  31913  mapdheq2  31919  mapdheq4lem  31921  mapdheq4  31922  mapdh6lem1N  31923  mapdh6lem2N  31924  mapdh6aN  31925  mapdh6bN  31927  mapdh6cN  31928  mapdh6dN  31929  mapdh6eN  31930  mapdh6fN  31931  mapdh6gN  31932  mapdh6hN  31933  mapdh6iN  31934  mapdh7eN  31938  mapdh7cN  31939  mapdh7dN  31940  mapdh7fN  31941  mapdh75e  31942  mapdh75fN  31945  hvmaplfl  31957  mapdhvmap  31959  mapdh8aa  31966  mapdh8ab  31967  mapdh8ad  31969  mapdh8b  31970  mapdh8c  31971  mapdh8d0N  31972  mapdh8d  31973  mapdh8e  31974  mapdh9a  31980  mapdh9aOLDN  31981  hdmap1val2  31991  hdmap1eq  31992  hdmap1valc  31994  hdmap1eq2  31996  hdmap1eq4N  31997  hdmap1l6lem1  31998  hdmap1l6lem2  31999  hdmap1l6a  32000  hdmap1l6b  32002  hdmap1l6c  32003  hdmap1l6d  32004  hdmap1l6e  32005  hdmap1l6f  32006  hdmap1l6g  32007  hdmap1l6h  32008  hdmap1l6i  32009  hdmap1eulem  32014  hdmap1eulemOLDN  32015  hdmap1neglem1N  32018  hdmapcl  32023  hdmapval2lem  32024  hdmapval0  32026  hdmapeveclem  32027  hdmapevec  32028  hdmapval3lemN  32030  hdmapval3N  32031  hdmap10lem  32032  hdmap11lem1  32034  hdmap11lem2  32035  hdmapnzcl  32038  hdmaprnlem3N  32043  hdmaprnlem3uN  32044  hdmaprnlem4N  32046  hdmaprnlem7N  32048  hdmaprnlem8N  32049  hdmaprnlem9N  32050  hdmaprnlem3eN  32051  hdmaprnlem16N  32055  hdmap14lem1  32061  hdmap14lem2N  32062  hdmap14lem3  32063  hdmap14lem4a  32064  hdmap14lem6  32066  hdmap14lem8  32068  hdmap14lem9  32069  hdmap14lem10  32070  hdmap14lem11  32071  hdmap14lem12  32072  hgmaprnlem1N  32089  hgmaprnlem2N  32090  hgmaprnlem3N  32091  hgmaprnlem4N  32092  hdmapip1  32109  hdmapinvlem1  32111  hdmapinvlem2  32112  hdmapinvlem3  32113  hdmapinvlem4  32114  hdmapglem5  32115  hgmapvvlem1  32116  hgmapvvlem2  32117  hgmapvvlem3  32118  hdmapglem7a  32120  hdmapglem7b  32121  hdmapglem7  32122
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155
  Copyright terms: Public domain W3C validator