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

Theorem eldifsni 4261
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 4260 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
21simprbi 479 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wne 2780  cdif 3537  {csn 4125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-v 3175  df-dif 3543  df-sn 4126
This theorem is referenced by:  neldifsn  4262  suppssov1  7214  suppss2  7216  suppssfv  7218  sniffsupp  8198  elfi2  8203  fifo  8221  en2other2  8715  finacn  8756  acndom2  8760  dfacacn  8846  kmlem11  8865  acncc  9145  axdc2lem  9153  1div0  10565  expne0i  12754  incexc  14408  fprodn0f  14561  oddprm  15353  firest  15916  symgextf1lem  17663  pmtrmvd  17699  efgsp1  17973  efgredlem  17983  gsummpt1n0  18187  dprdfid  18239  dprdres  18250  dprd2da  18264  dmdprdsplit2lem  18267  ablfac1b  18292  lvecinv  18934  lspsncmp  18937  lspsneq  18943  lspsneu  18944  lspdisjb  18947  lspexch  18950  lvecindp  18959  lvecindp2  18960  ringelnzr  19087  fidomndrnglem  19127  psrridm  19225  mplsubrg  19261  mplmon  19284  mplmonmul  19285  evlslem3  19335  coe1tmmul  19468  uvcff  19949  frlmssuvc2  19953  frlmup2  19957  lindfrn  19979  f1lindf  19980  dmatmul  20122  1marepvsma1  20208  mdetrsca2  20229  mdetrlin2  20232  mdetunilem5  20241  mdetunilem9  20245  maducoeval2  20265  gsummatr01lem3  20282  gsummatr01lem4  20283  gsummatr01  20284  ptpjpre2  21193  ptcmplem2  21667  i1fmullem  23267  itg1addlem4  23272  itg1addlem5  23273  i1fmulc  23276  itg1mulc  23277  i1fres  23278  itg10a  23283  itg1climres  23287  mbfi1fseqlem4  23291  ellimc2  23447  dvcnp2  23489  dvaddbr  23507  dvmulbr  23508  dvcobr  23515  dvcjbr  23518  dvrec  23524  dvcnvlem  23543  dvexp3  23545  dveflem  23546  ftc1lem6  23608  deg1n0ima  23653  ig1peu  23735  plyeq0lem  23770  dgrlem  23789  dgrlb  23796  coemulhi  23814  fta1  23867  aannenlem2  23888  tayl0  23920  taylthlem2  23932  abelthlem7  23996  dcubic  24373  rlimcnp  24492  efrlim  24496  muinv  24719  logexprlim  24750  lgslem1  24822  lgsqr  24876  lgseisenlem2  24901  lgseisenlem4  24903  lgseisen  24904  lgsquadlem1  24905  lgsquad2  24911  m1lgs  24913  dchrisum0re  25002  dchrisum0lema  25003  dchrisum0lem2  25007  dchrisum0lem3  25008  uhgrn0  25733  upgrn0  25756  upgrex  25759  umgran0  25849  umgraex  25852  cusgraexi  25997  frghash2spot  26590  1div0apr  26716  disjdsct  28863  signstfvneq0  29975  subfacp1lem1  30415  circum  30822  neibastop1  31524  bj-xpnzexb  32141  bj-restn0b  32225  curf  32557  poimirlem2  32581  poimirlem24  32603  poimirlem25  32604  dvtan  32630  ftc1cnnc  32654  ftc1anclem3  32657  rrndstprj2  32800  lshpne0  33291  lsatcv0  33336  lsat0cv  33338  lkreqN  33475  lkrlspeqN  33476  dochnel  35700  djhcvat42  35722  dochsnkr  35779  dochsnkr2cl  35781  lcfl6lem  35805  lcfl8b  35811  lcfrlem16  35865  lcfrlem25  35874  lcfrlem27  35876  lcfrlem33  35882  lcfrlem37  35886  mapdn0  35976  mapdpglem24  36011  mapdindp1  36027  mapdhval2  36033  hdmap1val2  36108  hdmapnzcl  36155  hdmap14lem1  36178  hdmap14lem4a  36181  hdmap14lem6  36183  hgmaprnlem1N  36206  hdmapip1  36226  hgmapvvlem1  36233  hgmapvvlem2  36234  aomclem2  36643  mpaaeu  36739  sdrgacs  36790  cntzsdrg  36791  deg1mhm  36804  clsk3nimkb  37358  gneispace  37452  radcnvrat  37535  bccm1k  37563  disjf1o  38373  icoiccdif  38597  climrec  38670  climdivf  38679  lptre2pt  38707  0ellimcdiv  38716  limclner  38718  reclimc  38720  divcncf  38769  cncficcgt0  38774  dvrecg  38800  fperdvper  38808  dvdivcncf  38817  dvnmul  38833  stoweidlem57  38950  dirkercncflem1  38996  fourierdlem24  39024  fourierdlem62  39061  fourierdlem66  39065  elaa2  39127  etransclem35  39162  etransclem47  39174  meadjiunlem  39358  ovnhoilem1  39491  hspmbllem1  39516  fmtnoprmfac1lem  40014  isuvtxa  40621  cusgrfilem2  40672  frgrhash2wsp  41497  lindssnlvec  42069  logcxp0  42127
  Copyright terms: Public domain W3C validator