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

Theorem eldifsni 3750
Description: Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
Assertion
Ref Expression
eldifsni  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )

Proof of Theorem eldifsni
StepHypRef Expression
1 eldifsn 3749 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
21simprbi 450 1  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684    =/= wne 2446    \ cdif 3149   {csn 3640
This theorem is referenced by:  neldifsn  3751  suppss2  6073  suppssfv  6074  suppssov1  6075  fofinf1o  7137  elfi2  7168  fifo  7185  finacn  7677  acndom2  7681  dfacacn  7767  kmlem11  7786  acncc  8066  axdc2lem  8074  1div0  9425  xrsupss  10627  expne0i  11134  incexc  12296  oddprm  12868  firest  13337  efgsp1  15046  efgredlem  15056  dprdfid  15252  dprdres  15263  dprd2da  15277  dmdprdsplit2lem  15280  ablfac1b  15305  lvecinv  15866  lspsncmp  15869  lspsneq  15875  lspsneu  15876  lspdisjb  15879  lspexch  15882  lvecindp  15891  lvecindp2  15892  rngelnzr  16017  fidomndrnglem  16047  psrridm  16149  mvridlem  16164  mplsubrg  16184  mplmon  16207  mplmonmul  16208  mplcoe3  16210  mplcoe2  16211  coe1tmmul  16353  ptpjpre2  17275  ptcmplem2  17747  i1fmullem  19049  itg1addlem4  19054  itg1addlem5  19055  i1fmulc  19058  itg1mulc  19059  i1fres  19060  itg10a  19065  itg1climres  19069  mbfi1fseqlem4  19073  ellimc2  19227  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvcobr  19295  dvcjbr  19298  dvrec  19304  dvcnvlem  19323  dvexp3  19325  dveflem  19326  ftc1lem6  19388  evlslem3  19398  deg1n0ima  19475  ig1peu  19557  plyeq0lem  19592  dgrlem  19611  dgrlb  19618  coemulhi  19635  fta1  19688  aannenlem2  19709  tayl0  19741  taylthlem2  19753  abelthlem7  19814  dcubic  20142  rlimcnp  20260  efrlim  20264  muinv  20433  logexprlim  20464  lgslem1  20535  lgsqr  20585  lgseisenlem2  20589  lgseisenlem4  20591  lgseisen  20592  lgsquadlem1  20593  lgsquad2  20599  m1lgs  20601  dchrisum0re  20662  dchrisum0lema  20663  dchrisum0lem2  20667  dchrisum0lem3  20668  1div0apr  20841  suppss2f  23201  disjdsct  23369  dmgmseqn0  23696  subfacp1lem1  23710  umgran0  23872  umgraex  23875  circum  24007  neibastop1  26308  rrndstprj2  26555  aomclem2  27152  uvcresum  27242  frlmssuvc2  27247  frlmup2  27251  lindfrn  27291  f1lindf  27292  mpaaeu  27355  en2other2  27382  pmtrmvd  27398  mamulid  27458  mamurid  27459  sdrgacs  27509  cntzsdrg  27510  deg1mhm  27526  climrec  27729  climdivf  27738  stoweidlem57  27806  lshpne0  29176  lsatcv0  29221  lsat0cv  29223  lkreqN  29360  lkrlspeqN  29361  dochnel  31583  djhcvat42  31605  dochsnkr  31662  dochsnkr2cl  31664  lcfl6lem  31688  lcfl8b  31694  lcfrlem16  31748  lcfrlem25  31757  lcfrlem27  31759  lcfrlem33  31765  lcfrlem37  31769  mapdn0  31859  mapdpglem24  31894  mapdindp1  31910  mapdhval2  31916  hdmap1val2  31991  hdmapnzcl  32038  hdmap14lem1  32061  hdmap14lem4a  32064  hdmap14lem6  32066  hgmaprnlem1N  32089  hdmapip1  32109  hgmapvvlem1  32116  hgmapvvlem2  32117
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-ne 2448  df-v 2790  df-dif 3155  df-sn 3646
  Copyright terms: Public domain W3C validator