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

Theorem eldifsni 4311
Description: Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
Assertion
Ref Expression
eldifsni (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴𝐶)

Proof of Theorem eldifsni
StepHypRef Expression
1 eldifsn 4308 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
21simprbi 480 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  wne 2791  cdif 3564  {csn 4168
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-v 3197  df-dif 3570  df-sn 4169
This theorem is referenced by:  neldifsn  4312  suppssov1  7312  suppss2  7314  suppssfv  7316  sniffsupp  8300  elfi2  8305  fifo  8323  en2other2  8817  finacn  8858  acndom2  8862  dfacacn  8948  kmlem11  8967  acncc  9247  axdc2lem  9255  1div0  10671  expne0i  12875  incexc  14550  fprodn0f  14703  oddprm  15496  firest  16074  symgextf1lem  17821  pmtrmvd  17857  efgsp1  18131  efgredlem  18141  gsummpt1n0  18345  dprdfid  18397  dprdres  18408  dprd2da  18422  dmdprdsplit2lem  18425  ablfac1b  18450  lvecinv  19094  lspsncmp  19097  lspsneq  19103  lspsneu  19104  lspdisjb  19107  lspexch  19110  lvecindp  19119  lvecindp2  19120  ringelnzr  19247  fidomndrnglem  19287  psrridm  19385  mplsubrg  19421  mplmon  19444  mplmonmul  19445  evlslem3  19495  coe1tmmul  19628  uvcff  20111  frlmssuvc2  20115  frlmup2  20119  lindfrn  20141  f1lindf  20142  dmatmul  20284  1marepvsma1  20370  mdetrsca2  20391  mdetrlin2  20394  mdetunilem5  20403  mdetunilem9  20407  maducoeval2  20427  gsummatr01lem3  20444  gsummatr01lem4  20445  gsummatr01  20446  ptpjpre2  21364  ptcmplem2  21838  divcncf  23197  i1fmullem  23442  itg1addlem4  23447  itg1addlem5  23448  i1fmulc  23451  itg1mulc  23452  i1fres  23453  itg10a  23458  itg1climres  23462  mbfi1fseqlem4  23466  ellimc2  23622  dvcnp2  23664  dvaddbr  23682  dvmulbr  23683  dvcobr  23690  dvcjbr  23693  dvrec  23699  dvrecg  23717  dvcnvlem  23720  dvexp3  23722  dveflem  23723  ftc1lem6  23785  deg1n0ima  23830  ig1peu  23912  plyeq0lem  23947  dgrlem  23966  dgrlb  23973  coemulhi  23991  fta1  24044  aannenlem2  24065  tayl0  24097  taylthlem2  24109  abelthlem7  24173  dcubic  24554  rlimcnp  24673  efrlim  24677  muinv  24900  logexprlim  24931  lgslem1  25003  lgsqr  25057  lgseisenlem2  25082  lgseisenlem4  25084  lgseisen  25085  lgsquadlem1  25086  lgsquad2  25092  m1lgs  25094  dchrisum0re  25183  dchrisum0lema  25184  dchrisum0lem2  25188  dchrisum0lem3  25189  uhgrn0  25943  upgrn0  25965  upgrex  25968  numedglnl  26020  upgrreslem  26177  isuvtxa  26276  cusgrexilem2  26319  cusgrexi  26320  structtocusgr  26323  cusgrfilem2  26333  frgrhash2wsp  27170  1div0apr  27294  disjdsct  29454  signstfvneq0  30623  subfacp1lem1  31135  circum  31542  neibastop1  32329  bj-xpnzexb  32923  bj-restn0b  33019  curf  33358  poimirlem2  33382  poimirlem24  33404  poimirlem25  33405  dvtan  33431  ftc1cnnc  33455  ftc1anclem3  33458  rrndstprj2  33601  lshpne0  34092  lsatcv0  34137  lsat0cv  34139  lkreqN  34276  lkrlspeqN  34277  dochnel  36501  djhcvat42  36523  dochsnkr  36580  dochsnkr2cl  36582  lcfl6lem  36606  lcfl8b  36612  lcfrlem16  36666  lcfrlem25  36675  lcfrlem27  36677  lcfrlem33  36683  lcfrlem37  36687  mapdn0  36777  mapdpglem24  36812  mapdindp1  36828  mapdhval2  36834  hdmap1val2  36909  hdmapnzcl  36956  hdmap14lem1  36979  hdmap14lem4a  36982  hdmap14lem6  36984  hgmaprnlem1N  37007  hdmapip1  37027  hgmapvvlem1  37034  hgmapvvlem2  37035  aomclem2  37444  mpaaeu  37539  sdrgacs  37590  cntzsdrg  37591  deg1mhm  37604  clsk3nimkb  38158  gneispace  38252  radcnvrat  38333  bccm1k  38361  disjf1o  39194  supminfxr2  39512  icoiccdif  39553  climrec  39635  climdivf  39644  lptre2pt  39672  0ellimcdiv  39681  limclner  39683  reclimc  39685  cncficcgt0  39864  fperdvper  39896  dvdivcncf  39905  dvnmul  39921  stoweidlem57  40037  dirkercncflem1  40083  fourierdlem24  40111  fourierdlem62  40148  fourierdlem66  40152  elaa2  40214  etransclem35  40249  etransclem47  40261  meadjiunlem  40445  ovnhoilem1  40578  hspmbllem1  40603  fmtnoprmfac1lem  41241  lindssnlvec  42040  logcxp0  42094
  Copyright terms: Public domain W3C validator