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

Theorem eldifsni 4466
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 4462 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
21simprbi 483 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  wne 2932  cdif 3712  {csn 4321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-v 3342  df-dif 3718  df-sn 4322
This theorem is referenced by:  neldifsn  4467  suppssov1  7496  suppss2  7498  suppssfv  7500  sniffsupp  8480  elfi2  8485  fifo  8503  en2other2  9022  finacn  9063  acndom2  9067  dfacacn  9155  kmlem11  9174  acncc  9454  axdc2lem  9462  1div0  10878  expne0i  13086  incexc  14768  fprodn0f  14921  oddprm  15717  firest  16295  symgextf1lem  18040  pmtrmvd  18076  efgsp1  18350  efgredlem  18360  gsummpt1n0  18564  dprdfid  18616  dprdres  18627  dprd2da  18641  dmdprdsplit2lem  18644  ablfac1b  18669  lvecinv  19315  lspsncmp  19318  lspsneq  19324  lspsneu  19325  lspdisjb  19328  lspexch  19331  lvecindp  19340  lvecindp2  19341  ringelnzr  19468  fidomndrnglem  19508  psrridm  19606  mplsubrg  19642  mplmon  19665  mplmonmul  19666  evlslem3  19716  coe1tmmul  19849  uvcff  20332  frlmssuvc2  20336  frlmup2  20340  lindfrn  20362  f1lindf  20363  dmatmul  20505  1marepvsma1  20591  mdetrsca2  20612  mdetrlin2  20615  mdetunilem5  20624  mdetunilem9  20628  maducoeval2  20648  gsummatr01lem3  20665  gsummatr01lem4  20666  gsummatr01  20667  ptpjpre2  21585  ptcmplem2  22058  divcncf  23416  i1fmullem  23660  itg1addlem4  23665  itg1addlem5  23666  i1fmulc  23669  itg1mulc  23670  i1fres  23671  itg10a  23676  itg1climres  23680  mbfi1fseqlem4  23684  ellimc2  23840  dvcnp2  23882  dvaddbr  23900  dvmulbr  23901  dvcobr  23908  dvcjbr  23911  dvrec  23917  dvrecg  23935  dvcnvlem  23938  dvexp3  23940  dveflem  23941  ftc1lem6  24003  deg1n0ima  24048  ig1peu  24130  plyeq0lem  24165  dgrlem  24184  dgrlb  24191  coemulhi  24209  fta1  24262  aannenlem2  24283  tayl0  24315  taylthlem2  24327  abelthlem7  24391  dcubic  24772  rlimcnp  24891  efrlim  24895  muinv  25118  logexprlim  25149  lgslem1  25221  lgsqr  25275  lgseisenlem2  25300  lgseisenlem4  25302  lgseisen  25303  lgsquadlem1  25304  lgsquad2  25310  m1lgs  25312  dchrisum0re  25401  dchrisum0lema  25402  dchrisum0lem2  25406  dchrisum0lem3  25407  uhgrn0  26161  upgrn0  26183  upgrex  26186  numedglnl  26238  upgrreslem  26395  isuvtx  26497  isuvtxaOLD  26498  cusgrexilem2  26548  cusgrexi  26549  structtocusgr  26552  cusgrfilem2  26562  frgrhash2wsp  27486  1div0apr  27635  disjdsct  29789  signstfvneq0  30958  subfacp1lem1  31468  circum  31875  neibastop1  32660  bj-xpnzexb  33254  bj-restn0b  33350  curf  33700  poimirlem2  33724  poimirlem24  33746  poimirlem25  33747  dvtan  33773  ftc1cnnc  33797  ftc1anclem3  33800  rrndstprj2  33943  lshpne0  34776  lsatcv0  34821  lsat0cv  34823  lkreqN  34960  lkrlspeqN  34961  dochnel  37184  djhcvat42  37206  dochsnkr  37263  dochsnkr2cl  37265  lcfl6lem  37289  lcfl8b  37295  lcfrlem16  37349  lcfrlem25  37358  lcfrlem27  37360  lcfrlem33  37366  lcfrlem37  37370  mapdn0  37460  mapdpglem24  37495  mapdindp1  37511  mapdhval2  37517  hdmap1val2  37592  hdmapnzcl  37639  hdmap14lem1  37662  hdmap14lem4a  37665  hdmap14lem6  37667  hgmaprnlem1N  37690  hdmapip1  37710  hgmapvvlem1  37717  hgmapvvlem2  37718  aomclem2  38127  mpaaeu  38222  sdrgacs  38273  cntzsdrg  38274  deg1mhm  38287  clsk3nimkb  38840  gneispace  38934  radcnvrat  39015  bccm1k  39043  disjf1o  39877  supminfxr2  40197  icoiccdif  40253  climrec  40338  climdivf  40347  lptre2pt  40375  0ellimcdiv  40384  limclner  40386  reclimc  40388  cnrefiisplem  40558  cncficcgt0  40604  fperdvper  40636  dvdivcncf  40645  dvnmul  40661  stoweidlem57  40777  dirkercncflem1  40823  fourierdlem24  40851  fourierdlem62  40888  fourierdlem66  40892  elaa2  40954  etransclem35  40989  etransclem47  41001  meadjiunlem  41185  ovnhoilem1  41321  hspmbllem1  41346  fmtnoprmfac1lem  41986  lindssnlvec  42785  logcxp0  42839
  Copyright terms: Public domain W3C validator