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

Theorem eldifsni 4721
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 4718 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
21simprbi 497 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wne 3021  cdif 3937  {csn 4564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-v 3502  df-dif 3943  df-sn 4565
This theorem is referenced by:  eldifsnneq  4722  neldifsn  4724  suppssov1  7858  suppss2  7860  suppssfv  7862  sniffsupp  8867  elfi2  8872  fifo  8890  en2other2  9429  finacn  9470  acndom2  9474  dfacacn  9561  kmlem11  9580  acncc  9856  axdc2lem  9864  1div0  11293  expne0i  13456  incexc  15187  fprodn0f  15340  oddprm  16142  firest  16701  symgextf1lem  18484  pmtrmvd  18520  efgsp1  18799  efgredlem  18809  gsummpt1n0  19021  dprdfid  19075  dprdres  19086  dprd2da  19100  dmdprdsplit2lem  19103  ablfac1b  19128  sdrgacs  19516  cntzsdrg  19517  lvecinv  19821  lspsncmp  19824  lspsneq  19830  lspsneu  19831  lspdisjb  19834  lspexch  19837  lvecindp2  19847  ringelnzr  19974  fidomndrnglem  20014  psrridm  20119  mplsubrg  20155  mplmon  20179  mplmonmul  20180  coe1tmmul  20380  uvcff  20870  frlmssuvc2  20874  frlmup2  20878  lindfrn  20900  f1lindf  20901  dmatmul  21041  1marepvsma1  21127  mdetrsca2  21148  mdetrlin2  21151  mdetunilem5  21160  mdetunilem9  21164  maducoeval2  21184  gsummatr01lem3  21201  gsummatr01lem4  21202  gsummatr01  21203  cmpfi  21951  ptpjpre2  22123  alexsublem  22587  ptcmplem2  22596  divcncf  23982  i1fmullem  24229  itg1addlem4  24234  itg1addlem5  24235  i1fmulc  24238  itg1mulc  24239  i1fres  24240  itg10a  24245  itg1climres  24249  mbfi1fseqlem4  24253  ellimc2  24409  dvcnp2  24451  dvaddbr  24469  dvmulbr  24470  dvcobr  24477  dvcjbr  24480  dvrec  24486  dvrecg  24504  dvcnvlem  24507  dvexp3  24509  dveflem  24510  ftc1lem6  24572  deg1n0ima  24617  ig1peu  24699  plyeq0lem  24734  dgrlem  24753  dgrlb  24760  coemulhi  24778  fta1  24831  aannenlem2  24852  tayl0  24884  taylthlem2  24896  abelthlem7  24960  dcubic  25356  rlimcnp  25476  efrlim  25480  muinv  25703  logexprlim  25734  lgslem1  25806  lgsqr  25860  lgseisenlem2  25885  lgseisenlem4  25887  lgseisen  25888  lgsquadlem1  25889  lgsquad2  25895  m1lgs  25897  dchrisum0re  26022  dchrisum0lema  26023  dchrisum0lem2  26027  dchrisum0lem3  26028  uhgrn0  26785  upgrn0  26807  upgrex  26810  numedglnl  26862  upgrreslem  27019  isuvtx  27110  cusgrexilem2  27157  cusgrexi  27158  structtocusgr  27161  cusgrfilem2  27171  frgrhash2wsp  28044  1div0apr  28180  disjdsct  30370  lindssn  30872  signstfvneq0  31747  lfuhgr2  32268  cusgredgex  32271  loop1cycl  32287  subfacp1lem1  32329  circum  32820  neibastop1  33610  bj-xpnzexb  34176  bj-restn0b  34282  curf  34756  poimirlem2  34780  poimirlem24  34802  poimirlem25  34803  dvtan  34828  ftc1cnnc  34852  ftc1anclem3  34855  rrndstprj2  34996  lsat0cv  36055  lkreqN  36192  lkrlspeqN  36193  dochnel  38415  djhcvat42  38437  dochsnkr  38494  dochsnkr2cl  38496  lcfl6lem  38520  lcfl8b  38526  lcfrlem16  38580  lcfrlem25  38589  lcfrlem27  38591  lcfrlem33  38597  lcfrlem37  38601  mapdn0  38691  mapdpglem24  38726  mapdindp1  38742  mapdhval2  38748  hdmap1val2  38822  hdmapnzcl  38867  hdmap14lem1  38890  hdmap14lem4a  38893  hdmap14lem6  38895  hgmaprnlem1N  38918  hdmapip1  38938  hgmapvvlem1  38945  hgmapvvlem2  38946  prjspersym  39141  prjspreln0  39143  prjspvs  39144  dffltz  39155  aomclem2  39539  mpaaeu  39634  deg1mhm  39691  gneispace  40368  radcnvrat  40530  bccm1k  40558  disjf1o  41336  supminfxr2  41629  icoiccdif  41684  climrec  41768  climdivf  41777  lptre2pt  41805  0ellimcdiv  41814  limclner  41816  reclimc  41818  cnrefiisplem  41994  cncficcgt0  42055  fperdvper  42087  dvdivcncf  42096  dvnmul  42112  stoweidlem57  42227  dirkercncflem1  42273  fourierdlem24  42301  fourierdlem62  42338  fourierdlem66  42342  elaa2  42404  etransclem35  42439  etransclem47  42451  meadjiunlem  42632  ovnhoilem1  42768  hspmbllem1  42793  fmtnoprmfac1lem  43577  lindssnlvec  44443  logcxp0  44497
  Copyright terms: Public domain W3C validator