Theorem eldifsni 4753

Description: Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)

Assertion

Ref	Expression
eldifsni	⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶)

Proof of Theorem eldifsni

Step	Hyp	Ref	Expression
1		eldifsn 4748	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
2	1	simprbi 503	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959   ∖ cdif 4048  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-dif 4050  df-sn 4589

This theorem is used by:  eldifsnneq  4754  neldifsn  4755  suppssov1  8239  suppssov2  8240  suppss2  8242  suppssfv  8244  curf  8915  sniffsupp  9416  elfi2  9430  fifo  9448  en2other2  10112  finacn  10153  acndom2  10157  dfacacn  10244  kmlem11  10263  acncc  10542  axdc2lem  10550  elfzodif0  13929  expne0i  14261  incexc  16032  fprodn0f  16184  oddprm  17014  firest  17629  pfxchn  18810  chnind  18821  chnccat  18826  chnrev  18827  symgextf1lem  19661  pmtrmvd  19697  efgsp1  19978  efgredlem  19988  gsummpt1n0  20206  dprdfid  20260  dprdres  20271  dprd2da  20285  dmdprdsplit2lem  20288  ablfac1b  20313  ringelnzr  20801  isdomn4  20994  isdrng4  21019  fidomndrnglem  21057  imadrhmcl  21081  sdrgacs  21085  cntzsdrg  21086  lvecinv  21418  lspsncmp  21421  lspsneq  21427  lspsneu  21428  lspdisjb  21431  lspexch  21434  lvecindp2  21444  drngidl  21566  cnflddiv  21735  uvcff  22124  frlmssuvc2  22128  frlmup2  22132  lindfrn  22154  f1lindf  22155  psrridm  22297  mplsubrg  22339  mplmon  22371  mplmonmul  22372  coe1tmmul  22623  dmatmul  22839  1marepvsma1  22925  mdetrsca2  22946  mdetrlin2  22949  mdetunilem5  22958  mdetunilem9  22962  maducoeval2  22982  gsummatr01lem3  22999  gsummatr01lem4  23000  gsummatr01  23001  cmpfi  23753  ptpjpre2  23926  alexsublem  24390  ptcmplem2  24399  divcn  25216  divcncf  25795  i1fmullem  26042  itg1addlem4  26047  itg1addlem5  26048  i1fmulc  26051  itg1mulc  26052  i1fres  26053  itg10a  26058  itg1climres  26062  mbfi1fseqlem4  26066  ellimc2  26224  dvcnp2  26267  dvaddbr  26285  dvmulbr  26286  dvcobr  26293  dvcjbr  26296  dvrec  26302  dvrecg  26320  dvcnvlem  26323  dvexp3  26325  dveflem  26326  ftc1lem6  26388  deg1n0ima  26434  ig1peu  26520  plyeq0lem  26556  dgrlem  26575  dgrlb  26582  coemulhi  26600  fta1  26656  preimaaa  26673  aannenlem2  26683  tayl0  26716  taylthlem2  26728  abelthlem7  26792  dcubic  27201  rlimcnp  27320  efrlim  27324  muinv  27547  logexprlim  27579  lgslem1  27651  lgsqr  27705  lgseisenlem2  27730  lgseisenlem4  27732  lgseisen  27733  lgsquad2  27740  m1lgs  27742  dchrisum0re  27867  dchrisum0lema  27868  dchrisum0lem2  27872  dchrisum0lem3  27873  nnne0s  28750  uhgrn0  29672  upgrn0  29694  upgrex  29697  numedglnl  29749  lfuhgr2  29754  upgrreslem  29912  isuvtx  30003  cusgrexilem2  30050  cusgrexi  30051  structtocusgr  30054  cusgrfilem2  30064  loop1cycl  30771  frgrhash2wsp  30960  1div0apr  31096  fmptunsnop  33361  disjdsct  33364  fxpsdrg  33803  elrgspnlem2  33871  elrgspnlem3  33872  domnprodn0  33906  fracfld  33937  lindssn  34000  pidufd  34142  1arithufdlem3  34145  dfufd2  34149  zringidom  34150  zringfrac  34153  deg1prod  34182  ig1pmindeg  34201  psrmonmul  34249  assafld  34336  irngnzply1  34390  irngnminplynz  34411  constrsdrg  34474  signstfvneq0  35268  cusgredgex  36062  subfacp1lem1  36110  circum  36605  neibastop1  37324  bj-xpnzexb  38051  bj-restn0b  38202  poimirlem2  38731  poimirlem24  38753  poimirlem25  38754  dvtan  38779  ftc1cnnc  38801  ftc1anclem3  38804  rrndstprj2  38956  lsat0cv  40281  lkreqN  40418  lkrlspeqN  40419  dochnel  42641  djhcvat42  42663  dochsnkr  42720  dochsnkr2cl  42722  lcfl6lem  42746  lcfl8b  42752  lcfrlem16  42806  lcfrlem25  42815  lcfrlem27  42817  lcfrlem33  42823  lcfrlem37  42827  mapdn0  42917  mapdpglem24  42952  mapdindp1  42968  mapdhval2  42974  hdmap1val2  43048  hdmapnzcl  43093  hdmap14lem1  43116  hdmap14lem4a  43119  hdmap14lem6  43121  hgmaprnlem1N  43144  hdmapip1  43164  hgmapvvlem1  43171  hgmapvvlem2  43172  aks6d1c5lem2  43379  resuppsinopn  43605  readvcot  43606  domnexpgn0cl  43775  prjspersym  43826  prjspreln0  43828  prjspvs  43829  dffltz  43861  aomclem2  44248  mpaaeu  44342  deg1mhm  44392  gneispace  45324  radcnvrat  45488  bccm1k  45516  disjf1o  46409  supminfxr2  46682  icoiccdif  46739  climrec  46818  climdivf  46827  lptre2pt  46853  0ellimcdiv  46862  limclner  46864  reclimc  46866  cnrefiisplem  47042  cncficcgt0  47101  fperdvper  47132  dvdivcncf  47140  dvnmul  47156  stoweidlem57  47270  dirkercncflem1  47316  fourierdlem24  47344  fourierdlem62  47381  fourierdlem66  47385  elaa2  47447  etransclem35  47482  etransclem47  47494  meadjiunlem  47678  ovnhoilem1  47814  hspmbllem1  47839  fmtnoprmfac1lem  48852  isubgruhgr  49169  isubgr0uhgr  49174  lindssnlvec  49801  logcxp0  49850