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

Theorem eldifi 3576
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 3436 . 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 1758    \ cdif 3423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3070  df-dif 3429
This theorem is referenced by:  difss  3581  noel  3739  tz7.7  4843  tfi  6564  peano5  6599  tz7.48-1  6998  tz7.49  7000  dif20el  7045  oaf1o  7102  oeordi  7126  oeord  7127  oecan  7128  oeword  7129  oeworde  7132  oelimcl  7139  oeeulem  7140  oeeui  7141  oaabs2  7184  boxcutc  7406  domdifsn  7494  isinf  7627  pssnn  7632  pwfilem  7706  fsuppco2  7753  fsuppcor  7754  ordtypelem7  7839  unxpwdom2  7904  inf3lem3  7937  cantnfp1lem1  7987  cantnfp1lem3  7989  cantnfp1lem1OLD  8013  cantnfp1lem3OLD  8015  infxpenc2lem1  8286  dfacacn  8411  isf32lem3  8625  isf34lem4  8647  fin67  8665  isfin7-2  8666  domtriomlem  8712  axdc2lem  8718  axdc3lem4  8723  axdc4lem  8725  ttukeylem7  8785  konigthlem  8833  fpwwe2lem13  8910  fpwwe2  8911  hashf1lem1  12310  rlimrege0  13159  rlimrecl  13160  sumrblem  13290  fsumcvg  13291  summolem2a  13294  fsumss  13304  fsumless  13361  cvgcmpce  13383  binomlem  13394  incexclem  13401  incexc  13402  isumltss  13413  rpnnen2lem10  13608  rpnnen2lem11  13609  oddprm  13984  iserodd  14004  prmreclem2  14080  prmreclem3  14081  prmreclem5  14083  4sqlem19  14126  prmlem0  14235  firest  14473  grpinvnzcl  15700  symgextfv  16025  pmtrf  16063  pmtrdifellem3  16086  sylow2alem2  16221  sylow2a  16222  efgsf  16330  efgsrel  16335  efgs1  16336  efgsfo  16340  efgredlemc  16346  gsumzaddlem  16512  gsumzadd  16513  gsumzaddlemOLD  16514  gsumzaddOLD  16515  gsumzmhm  16535  gsumzmhmOLD  16536  gsumzinvOLD  16548  gsumsubOLD  16553  gsum2d2lem  16570  dprdfadd  16615  dprdfaddOLD  16622  dprdres  16630  subgdmdprd  16636  dmdprdsplitlem  16639  dmdprdsplitlemOLD  16640  dmdprdsplit2lem  16649  dpjidcl  16662  dpjidclOLD  16669  ablfac1b  16676  pgpfac1lem1  16680  gsummgp0  16805  isirred  16897  irredrmul  16905  isdrng2  16948  isdrngd  16963  lcomfsupOLD  17090  lcomfsupp  17091  lbspropd  17286  lspsneq  17309  lsppratlem6  17339  lbsextlem2  17346  lbsextlem4  17348  rngelnzr  17453  psrbaglesupp  17541  psrbaglesuppOLD  17542  psrlidm  17580  psrlidmOLD  17581  psrridm  17582  psrridmOLD  17583  mplsubglem  17617  mpllsslem  17618  mplsubglemOLD  17619  mpllsslemOLD  17620  mplsubrglem  17624  mplsubrglemOLD  17625  mplmonmul  17650  mplcoe1  17651  mplcoe5  17655  mplcoe2OLD  17657  mplbas2  17658  mplbas2OLD  17659  evlslem3  17707  coe1tmmul2  17837  coe1tmmul  17838  xrs1mnd  17960  xrs10  17961  xrs1cmn  17962  cnsubrg  17982  psgnodpm  18127  zrhpsgnodpm  18131  evpmodpmf1o  18135  uvcresum  18327  frlmssuvc1  18328  frlmssuvc1OLD  18330  frlmsslsp  18332  frlmsslspOLD  18333  frlmup2  18336  lindfrn  18359  f1lindf  18360  lindfmm  18365  islindf4  18376  1marepvsma1  18505  mdetdiaglem  18520  mdetrlin  18524  mdetrsca  18525  mdetralt  18530  maducoeval2  18562  madugsum  18565  symgmatr01  18576  gsummatr01lem3  18579  gsummatr01lem4  18580  gsummatr01  18581  smadiadetlem0  18583  smadiadetlem1a  18585  cmpfi  19127  2ndcdisj2  19177  elptr2  19263  ptcnplem  19310  xkopt  19344  kqdisj  19421  fin1aufil  19621  ptcmplem2  19741  ptcmplem3  19742  ptcmplem4  19743  opnsubg  19794  lpbl  20194  blcld  20196  zcld  20506  recld2  20507  reconnlem1  20519  divcn  20560  iundisj  21145  mbfeqalem  21236  itg1val2  21278  itg1ge0  21280  i1fmullem  21288  i1fadd  21289  itg1addlem4  21293  itg1mulc  21298  itg1lea  21306  itg1le  21307  mbfi1fseqlem4  21312  itg2uba  21337  itg2lea  21338  itg2eqa  21339  itg2splitlem  21342  itg2split  21343  itgeqa  21407  ellimc3  21470  dvaddbr  21528  dvmulbr  21529  dvcobr  21536  dvcjbr  21539  dvrec  21545  dvcnvlem  21564  dvexp3  21566  dveflem  21567  tdeglem4  21645  deg1n0ima  21676  deg1mul3le  21704  ig1peu  21759  ply1termlem  21787  plypf1  21796  plyaddlem1  21797  plymullem1  21798  coeeulem  21808  coeidlem  21821  coeid3  21824  coefv0  21831  coemulhi  21837  coemulc  21838  dvply1  21866  fta1  21890  vieta1lem2  21893  elaa  21898  elqaalem2  21902  aannenlem2  21911  aaliou2  21922  tayl0  21943  dvtaylp  21951  taylthlem1  21954  taylthlem2  21955  pserdvlem2  22009  dcubic  22357  rlimcnp  22475  jensen  22498  wilthlem2  22523  basellem3  22536  chpub  22675  logexprlim  22680  lgslem1  22751  lgslem4  22754  lgsvalmod  22770  lgsqr  22801  lgsquadlem1  22809  lgsquad2  22815  m1lgs  22817  dchrisum0fno1  22876  rplogsum  22892  cusgraexi  23511  uvtxnbgra  23536  cusconngra  23697  ablomul  23977  mulid  23978  zerdivemp1  24056  strlem1  25789  strlem3  25792  strlem4  25793  strlem5  25794  hstrlem3  25800  hstrlem4  25801  iundisjf  26065  iundisjfi  26214  elzdif0  26543  logbcl  26590  ind0  26610  measvunilem  26760  eulerpartlemb  26885  eulerpartlemf  26887  sseqf  26909  ballotlem5  27016  ballotlemi1  27019  ballotlemii  27020  ballotlemic  27023  ballotlem1c  27024  ballotlemscr  27035  ballotlemro  27039  ballotlemfg  27042  ballotlemfrc  27043  ballotlemfrceq  27045  ballotlemrinv0  27049  plymulx0  27082  signstfvn  27104  dmgmaddn0  27143  dmlogdmgm  27144  lgamgulmlem2  27150  igamz  27168  gamp1  27178  regamcl  27181  subfacp1lem1  27201  circum  27453  prodrblem  27576  fprodcvg  27577  prodmolem2a  27581  fprodss  27595  dfon2lem6  27735  wfrlem10  27867  wfrlem15  27872  dvtan  28580  itg2addnclem2  28582  ftc1cnnc  28604  dvasin  28618  dvreasin  28620  dvreacos  28621  neibastop1  28718  isdrngo2  28902  isdrngo3  28903  divrngidl  28966  isfldidl  29006  pridlc2  29010  pridlc3  29011  prter2  29164  irrapx1  29307  pell1234qrne0  29332  pell1234qrreccl  29333  pell1234qrmulcl  29334  pell14qrgt0  29338  pell1234qrdich  29340  pell14qrdich  29348  pell1qrge1  29349  pell1qr1  29350  pell1qrgap  29353  pell14qrgapw  29355  pellqrexplicit  29356  pellqrex  29358  pellfundge  29361  pellfundgt1  29362  setindtr  29511  kelac1  29554  mpaaeu  29645  flcidc  29669  cntzsdrg  29697  deg1mhm  29713  climrec  29914  stoweidlem25  29958  stoweidlem28  29961  stoweidlem41  29974  stoweidlem44  29977  stoweidlem46  29979  stirlinglem5  30011  fsummsndifre  30375  fsummmodsndifre  30377  frgrancvvdeqlem9  30772  frgrancvvdeq  30773  frgrancvvdgeq  30774  2spotiundisj  30793  frghash2spot  30794  mgpsumunsn  30897  mgpsumz  30898  mgpsumn  30899  dmatmul  31030  lindslinindsimp1  31098  lindslinindsimp2  31104  lincresunit1  31118  lincresunit2  31119  lincresunit3lem1  31120  lincresunit3lem2  31121  lincresunit3  31122  lindssnlvec  31127  elogb  31406  bnj923  32061  bnj570  32198  bnj594  32205  lsateln0  32946  lsatlss  32947  lsmsat  32959  lsatcv0  32982  lsat0cv  32984  lcv1  32992  l1cvpat  33005  dih1dimatlem  35280  dihatexv2  35290  djhcvat42  35366  dihjat1lem  35379  dochsatshp  35402  lcfl6  35451  mapdrvallem2  35596  mapdpglem32  35656  mapdh9aOLDN  35742  hdmap1eulemOLDN  35776
  Copyright terms: Public domain W3C validator