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

Theorem eldifsni 4257
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 4256 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
21simprbi 478 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wne 2776  cdif 3533  {csn 4121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-v 3171  df-dif 3539  df-sn 4122
This theorem is referenced by:  neldifsn  4258  suppssov1  7188  suppss2  7190  suppssfv  7192  sniffsupp  8172  elfi2  8177  fifo  8195  en2other2  8689  finacn  8730  acndom2  8734  dfacacn  8820  kmlem11  8839  acncc  9119  axdc2lem  9127  1div0  10532  expne0i  12706  incexc  14351  fprodn0f  14504  oddprm  15296  firest  15859  symgextf1lem  17606  pmtrmvd  17642  efgsp1  17916  efgredlem  17926  gsummpt1n0  18130  dprdfid  18182  dprdres  18193  dprd2da  18207  dmdprdsplit2lem  18210  ablfac1b  18235  lvecinv  18877  lspsncmp  18880  lspsneq  18886  lspsneu  18887  lspdisjb  18890  lspexch  18893  lvecindp  18902  lvecindp2  18903  ringelnzr  19030  fidomndrnglem  19070  psrridm  19168  mplsubrg  19204  mplmon  19227  mplmonmul  19228  evlslem3  19278  coe1tmmul  19411  uvcff  19888  frlmssuvc2  19892  frlmup2  19896  lindfrn  19918  f1lindf  19919  dmatmul  20061  1marepvsma1  20147  mdetrsca2  20168  mdetrlin2  20171  mdetunilem5  20180  mdetunilem9  20184  maducoeval2  20204  gsummatr01lem3  20221  gsummatr01lem4  20222  gsummatr01  20223  ptpjpre2  21132  ptcmplem2  21606  i1fmullem  23181  itg1addlem4  23186  itg1addlem5  23187  i1fmulc  23190  itg1mulc  23191  i1fres  23192  itg10a  23197  itg1climres  23201  mbfi1fseqlem4  23205  ellimc2  23361  dvcnp2  23403  dvaddbr  23421  dvmulbr  23422  dvcobr  23429  dvcjbr  23432  dvrec  23438  dvcnvlem  23457  dvexp3  23459  dveflem  23460  ftc1lem6  23522  deg1n0ima  23567  ig1peu  23649  plyeq0lem  23684  dgrlem  23703  dgrlb  23710  coemulhi  23728  fta1  23781  aannenlem2  23802  tayl0  23834  taylthlem2  23846  abelthlem7  23910  dcubic  24287  rlimcnp  24406  efrlim  24410  muinv  24633  logexprlim  24664  lgslem1  24736  lgsqr  24790  lgseisenlem2  24815  lgseisenlem4  24817  lgseisen  24818  lgsquadlem1  24819  lgsquad2  24825  m1lgs  24827  dchrisum0re  24916  dchrisum0lema  24917  dchrisum0lem2  24921  dchrisum0lem3  24922  umgran0  25612  umgraex  25615  cusgraexi  25760  frghash2spot  26353  1div0apr  26479  disjdsct  28666  signstfvneq0  29778  subfacp1lem1  30218  circum  30625  neibastop1  31327  bj-xpnzexb  31941  bj-restn0b  32025  curf  32357  poimirlem2  32381  poimirlem24  32403  poimirlem25  32404  dvtan  32430  ftc1cnnc  32454  ftc1anclem3  32457  rrndstprj2  32600  lshpne0  33091  lsatcv0  33136  lsat0cv  33138  lkreqN  33275  lkrlspeqN  33276  dochnel  35500  djhcvat42  35522  dochsnkr  35579  dochsnkr2cl  35581  lcfl6lem  35605  lcfl8b  35611  lcfrlem16  35665  lcfrlem25  35674  lcfrlem27  35676  lcfrlem33  35682  lcfrlem37  35686  mapdn0  35776  mapdpglem24  35811  mapdindp1  35827  mapdhval2  35833  hdmap1val2  35908  hdmapnzcl  35955  hdmap14lem1  35978  hdmap14lem4a  35981  hdmap14lem6  35983  hgmaprnlem1N  36006  hdmapip1  36026  hgmapvvlem1  36033  hgmapvvlem2  36034  aomclem2  36443  mpaaeu  36539  sdrgacs  36590  cntzsdrg  36591  deg1mhm  36604  clsk3nimkb  37158  gneispace  37252  radcnvrat  37335  bccm1k  37363  disjf1o  38173  icoiccdif  38398  climrec  38471  climdivf  38480  lptre2pt  38508  0ellimcdiv  38517  limclner  38519  reclimc  38521  divcncf  38570  cncficcgt0  38575  dvrecg  38601  fperdvper  38609  dvdivcncf  38618  dvnmul  38634  stoweidlem57  38751  dirkercncflem1  38797  fourierdlem24  38825  fourierdlem62  38862  fourierdlem66  38866  elaa2  38928  etransclem35  38963  etransclem47  38975  meadjiunlem  39159  ovnhoilem1  39292  hspmbllem1  39317  fmtnoprmfac1lem  39816  uhgrn0  40288  upgrn0  40314  upgrex  40317  isuvtxa  40620  cusgrfilem2  40671  frgrhash2wsp  41496  lindssnlvec  42068  logcxp0  42126
  Copyright terms: Public domain W3C validator