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

Theorem eldifsni 4022
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 4021 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
21simprbi 464 1  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    =/= wne 2620    \ cdif 3346   {csn 3898
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 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-v 2995  df-dif 3352  df-sn 3899
This theorem is referenced by:  neldifsn  4023  suppss2OLD  6336  suppssfvOLD  6337  suppssov1OLD  6338  suppssov1  6742  suppss2  6744  suppssfv  6746  sniffsupp  7680  elfi2  7685  fifo  7703  en2other2  8197  finacn  8241  acndom2  8245  dfacacn  8331  kmlem11  8350  acncc  8630  axdc2lem  8638  1div0  10016  expne0i  11917  incexc  13321  oddprm  13903  firest  14392  symgextf1lem  15946  pmtrmvd  15983  efgsp1  16255  efgredlem  16265  gsummpt1n0  16478  dprdfid  16529  dprdfidOLD  16536  dprdres  16547  dprd2da  16563  dmdprdsplit2lem  16566  ablfac1b  16593  lvecinv  17216  lspsncmp  17219  lspsneq  17225  lspsneu  17226  lspdisjb  17229  lspexch  17232  lvecindp  17241  lvecindp2  17242  rngelnzr  17369  fidomndrnglem  17400  psrridm  17498  psrridmOLD  17499  mvridlemOLD  17514  mplsubrg  17541  mplmon  17564  mplmonmul  17565  mplcoe3OLD  17568  mplcoe2OLD  17572  evlslem3  17622  coe1tmmul  17752  uvcff  18238  frlmssuvc2  18242  frlmssuvc2OLD  18244  frlmup2  18249  lindfrn  18272  f1lindf  18273  1marepvsma1  18416  mdetrsca2  18433  mdetrlin2  18435  mdetunilem5  18444  mdetunilem9  18448  maducoeval2  18468  gsummatr01lem3  18485  gsummatr01lem4  18486  gsummatr01  18487  ptpjpre2  19175  ptcmplem2  19647  i1fmullem  21194  itg1addlem4  21199  itg1addlem5  21200  i1fmulc  21203  itg1mulc  21204  i1fres  21205  itg10a  21210  itg1climres  21214  mbfi1fseqlem4  21218  ellimc2  21374  dvcnp2  21416  dvaddbr  21434  dvmulbr  21435  dvcobr  21442  dvcjbr  21445  dvrec  21451  dvcnvlem  21470  dvexp3  21472  dveflem  21473  ftc1lem6  21535  deg1n0ima  21582  ig1peu  21665  plyeq0lem  21700  dgrlem  21719  dgrlb  21726  coemulhi  21743  fta1  21796  aannenlem2  21817  tayl0  21849  taylthlem2  21861  abelthlem7  21925  dcubic  22263  rlimcnp  22381  efrlim  22385  muinv  22555  logexprlim  22586  lgslem1  22657  lgsqr  22707  lgseisenlem2  22711  lgseisenlem4  22713  lgseisen  22714  lgsquadlem1  22715  lgsquad2  22721  m1lgs  22723  dchrisum0re  22784  dchrisum0lema  22785  dchrisum0lem2  22789  dchrisum0lem3  22790  umgran0  23276  umgraex  23279  cusgraexi  23398  1div0apr  23683  suppss2f  25976  disjdsct  26020  subfacp1lem1  27089  circum  27341  dvtan  28468  ftc1cnnc  28492  ftc1anclem3  28495  neibastop1  28606  rrndstprj2  28756  aomclem2  29434  mpaaeu  29533  sdrgacs  29584  cntzsdrg  29585  deg1mhm  29601  climrec  29802  climdivf  29811  stoweidlem57  29878  frghash2spot  30682  dmatmul  30915  lindssnlvec  31017  elogb  31206  bj-xpnzexb  32549  lshpne0  32727  lsatcv0  32772  lsat0cv  32774  lkreqN  32911  lkrlspeqN  32912  dochnel  35134  djhcvat42  35156  dochsnkr  35213  dochsnkr2cl  35215  lcfl6lem  35239  lcfl8b  35245  lcfrlem16  35299  lcfrlem25  35308  lcfrlem27  35310  lcfrlem33  35316  lcfrlem37  35320  mapdn0  35410  mapdpglem24  35445  mapdindp1  35461  mapdhval2  35467  hdmap1val2  35542  hdmapnzcl  35589  hdmap14lem1  35612  hdmap14lem4a  35615  hdmap14lem6  35617  hgmaprnlem1N  35640  hdmapip1  35660  hgmapvvlem1  35667  hgmapvvlem2  35668
  Copyright terms: Public domain W3C validator