Theorem eldifsn 4730

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

Assertion

Ref	Expression
eldifsn	⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Proof of Theorem eldifsn

Step	Hyp	Ref	Expression
1		eldif 3900	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4582	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2970	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 574	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 275	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933   ∖ cdif 3887  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-sn 4569

This theorem is referenced by:  eldifsnd  4731  eldifsni  4734  rexdifsn  4738  raldifsni  4739  eldifvsn  4741  difsn  4742  sossfld  6148  tpres  7153  onmindif2  7758  xpord3pred  8099  xpord3inddlem  8101  mptsuppd  8134  suppssr  8142  suppssov1  8144  suppssov2  8145  suppsssn  8148  suppssfv  8149  dif1o  8432  difsnen  8994  limenpsi  9087  frfi  9192  fofinf1o  9239  en2eleq  9927  en2other2  9928  dfac8clem  9951  acni2  9965  acndom  9970  acnnum  9971  dfac9  10056  dfacacn  10061  kmlem3  10072  kmlem4  10073  fin23lem21  10258  canthp1lem2  10573  elni  10796  mulnzcnf  11793  divval  11808  elnnne0  12448  elq  12897  rpcndif0  12960  modfzo0difsn  13902  modsumfzodifsn  13903  expcl2lem  14032  expclzlem  14042  hashdifpr  14374  hashgt23el  14383  prprrab  14432  hashle2prv  14437  reccn2  15556  rlimdiv  15605  eff2  16063  tanval  16092  rpnnen2lem9  16186  fzo0dvdseq  16289  oddprmgt2  16666  oddprmdvds  16871  4sqlem19  16931  prmlem0  17073  prmlem1a  17074  setsnid  17175  grpinvnzcl  18984  symgextf  19389  f1omvdmvd  19415  pmtrprfv  19425  odcau  19576  efgsf  19701  efgsrel  19706  efgs1  19707  efgs1b  19708  efgsp1  19709  efgsres  19710  efgredlema  19712  efgredlemd  19716  efgrelexlemb  19722  gsumpt  19934  dmdprdd  19973  dprdcntz  19982  dprdfeq0  19996  dprd2da  20016  isdomn2OLD  20686  domnrrg  20687  isdomn3  20689  drngunit  20708  isdrng2  20717  drngmcl  20724  drngid2  20726  isdrngd  20739  isdrngdOLD  20741  issubdrg  20754  sdrgacs  20775  cntzsdrg  20776  islss  20926  lssneln0  20945  lssssr  20946  lbsind  21073  lbspss  21075  lspabs3  21117  lspsneq  21118  lspfixed  21124  lspexch  21125  islbs2  21150  cnflddivOLD  21397  cnfldinv  21398  cnsubdrglem  21414  cnmgpid  21425  cnmsubglem  21426  gzrngunit  21429  xrs1mnd  21436  xrs10  21437  xrge0subm  21439  zringunit  21462  zringndrg  21464  domnchr  21528  cnmsgngrp  21575  psgninv  21578  psgndiflemB  21596  lindfind  21812  lindsind  21813  lindff1  21816  lindfrn  21817  mvrcl  21986  coe1tmmul2  22257  mdetunilem9  22601  maducoeval2  22621  gsummatr01lem4  22639  ist1-2  23328  cmpfi  23389  2ndcdisj  23437  2ndcsep  23440  locfincmp  23507  alexsublem  24025  cldsubg  24092  imasdsf1olem  24354  prdsxmslem2  24510  reperflem  24800  xrge0gsumle  24815  xrge0tsms  24816  divcn  24851  evth  24942  cvsdiv  25115  cvsdivcl  25116  cphreccllem  25161  bcthlem5  25311  itg11  25674  i1fmullem  25677  i1fadd  25678  itg1addlem2  25680  i1fmulc  25686  itg1mulc  25687  ellimc3  25862  limcmpt2  25867  dvlem  25879  dvidlem  25898  dvcnp  25902  dvcobr  25929  dvrec  25938  dvrecg  25956  dvmptdiv  25957  dvcnvlem  25959  dvexp3  25961  dveflem  25962  dvferm1lem  25967  dvferm2lem  25969  lhop1lem  25996  ftc1lem5  26023  mdegleb  26045  coe1mul3  26080  ply1nz  26103  fta1blem  26152  fta1b  26153  ig1peu  26156  ig1pdvds  26161  plyeq0lem  26191  dgrub  26215  quotval  26275  fta1lem  26290  fta1  26291  elqaalem3  26304  qaa  26306  iaa  26308  aareccl  26309  aannenlem2  26312  abelthlem8  26423  abelth  26425  eff1olem  26531  logrncl  26550  eflog  26559  logeftb  26566  logdmss  26625  dvlog  26634  logbcl  26750  logbid1  26751  logb1  26752  elogb  26753  logbchbase  26754  relogbval  26755  relogbcl  26756  relogbreexp  26758  relogbmul  26760  nnlogbexp  26764  relogbcxp  26768  cxplogb  26769  relogbcxpb  26770  logbf  26772  logblog  26775  2logb9irrALT  26781  sqrt2cxp2logb9e3  26782  angval  26784  dcubic  26829  rlimcnp  26948  efrlim  26952  efrlimOLD  26953  logexprlim  27208  dchrghm  27239  dchrabs  27243  lgsfcl2  27286  lgsval2lem  27290  lgsval3  27298  lgsmod  27306  lgsdirprm  27314  lgsne0  27318  gausslemma2dlem0f  27344  lgsquad2lem2  27368  2lgsoddprm  27399  2sqlem11  27412  2sqblem  27414  dchrvmaeq0  27487  rpvmasum2  27495  dchrisum0re  27496  qrngdiv  27607  addsval  27974  divsval  28201  elnns  28352  1nns  28361  tglngval  28639  tgisline  28715  axlowdimlem9  29039  axlowdimlem12  29042  axlowdimlem13  29043  elntg2  29074  upgrbi  29182  upgr1elem  29201  umgrislfupgrlem  29211  edgupgr  29223  subgruhgredgd  29373  upgrreslem  29393  nbgrel  29429  nbupgr  29433  nbupgrel  29434  nbumgrvtx  29435  nbgrssovtx  29450  nbupgrres  29453  nbusgrvtxm1uvtx  29494  nbupgruvtxres  29496  iscplgredg  29506  cusgredg  29513  cusgrfilem2  29546  usgredgsscusgredg  29549  1loopgrnb0  29592  1egrvtxdg0  29601  uhgrvd00  29624  vtxdginducedm1lem4  29632  eupth2lem3lem3  30321  frcond1  30357  frcond4  30361  2pthfrgr  30375  3cyclfrgrrn1  30376  n4cyclfrgr  30382  frgrwopreglem4a  30401  numclwwlk5  30479  ressupprn  32784  suppss3  32817  xdivval  32999  xrge0tsmsd  33155  pmtrcnel  33171  pmtrcnelor  33173  0nellinds  33451  dvdsruasso  33466  mxidlirredi  33552  extdg1id  33832  irngnzply1  33857  submatminr1  33976  ordtconnlem1  34090  ispisys2  34319  sigapisys  34321  sibfinima  34505  sseqf  34558  signswch  34727  signstfvn  34735  signsvtn0  34736  signstfvneq0  34738  signstfvcl  34739  signstfveq0a  34742  signstfveq0  34743  signsvfn  34748  signsvtp  34749  signsvtn  34750  signsvfpn  34751  signsvfnn  34752  signlem0  34753  bnj158  34894  bnj168  34895  bnj529  34906  bnj906  35094  bnj970  35111  exdifsn  35243  cusgredgex2  35327  subfacp1lem5  35388  cvmsi  35469  cvmsval  35470  cvmsdisj  35474  cvmscld  35477  cvmsss2  35478  satfv1lem  35566  sinccvglem  35876  circum  35878  mpomulnzcnf  36503  unbdqndv2lem2  36792  bj-0int  37435  lindsadd  37956  lindsenlbs  37958  matunitlindflem2  37960  matunitlindf  37961  poimirlem6  37969  poimirlem7  37970  poimirlem8  37971  poimirlem16  37979  poimirlem18  37981  poimirlem19  37982  poimirlem21  37984  poimirlem22  37985  poimirlem24  37987  poimirlem25  37988  poimirlem26  37989  poimirlem27  37990  itg2addnclem2  38015  sdclem1  38086  rrncmslem  38175  rrnequiv  38178  isdrngo2  38301  isdrngo3  38302  eldmxrncnvepres  38777  eldmxrncnvepres2  38778  prtlem100  39327  prter2  39349  prter3  39350  lsatlspsn2  39460  lsateln0  39463  lsatn0  39467  lsatspn0  39468  lsatcmp  39471  lsatelbN  39474  islshpat  39485  lsat0cv  39501  lkrlspeqN  39639  dvheveccl  41580  dihlatat  41805  dochnel  41861  dihjat1  41897  dvh4dimlem  41911  dochsnkr2cl  41942  dochkr1  41946  dochkr1OLDN  41947  lcfl6lem  41966  lcfl9a  41973  lclkrlem2l  41986  lclkrlem2o  41989  lclkrlem2q  41991  lcfrlem9  42018  lcfrlem16  42026  lcfrlem17  42027  lcfrlem27  42037  lcfrlem37  42047  lcfrlem38  42048  lcfrlem40  42050  lcdlkreqN  42090  mapdrvallem2  42113  mapdn0  42137  mapdpglem20  42159  mapdpglem30  42170  mapdindp0  42187  mapdhcl  42195  mapdh6aN  42203  mapdh6dN  42207  mapdh6eN  42208  mapdh6kN  42214  mapdh8  42256  hdmap1l6a  42277  hdmap1l6d  42281  hdmap1l6e  42282  hdmap1l6k  42288  hdmapval3N  42306  hdmap10  42308  hdmap11lem2  42310  hdmapnzcl  42313  hdmaprnlem3eN  42326  hdmaprnlem17N  42331  hdmap14lem4a  42339  hdmap14lem7  42342  hdmap14lem14  42349  hgmaprnlem5N  42368  hdmaplkr  42381  hdmapip0  42383  hgmapvvlem2  42392  hgmapvvlem3  42393  hgmapvv  42394  redvmptabs  42814  readvrec2  42815  readvrec  42816  fiabv  43003  fsuppind  43045  0prjspnlem  43078  pellexlem5  43287  dfac11  43516  dfacbasgrp  43562  dgraalem  43599  dgraaub  43602  aaitgo  43616  proot1ex  43650  deg1mhm  43654  ofdivrec  44779  ofdivcan4  44780  ofdivdiv2  44781  expgrowth  44788  binomcxplemnotnn0  44809  dvdivbd  46377  dvdivcncf  46381  dirkeritg  46556  fourierdlem39  46600  fourierdlem57  46617  fourierdlem58  46618  fourierdlem59  46619  fourierdlem68  46628  fourierdlem76  46636  fourierdlem103  46663  fourierdlem104  46664  fourierdlem111  46671  setsnidel  47857  sprvalpwn0  47963  odz2prm2pw  48046  fmtnoprmfac1  48048  fmtnoprmfac2  48050  sfprmdvdsmersenne  48086  lighneallem2  48089  lighneallem3  48090  lighneal  48094  oddprmALTV  48183  evenprm2  48210  oddprmne2  48211  odd2prm2  48214  even3prm2  48215  isubgruhgr  48364  grimuhgr  48383  2zrngnmrid  48752  lincext1  48950  lindslinindsimp2lem5  48958  rege1logbrege0  49054  fllogbd  49056  relogbmulbexp  49057  relogbdivb  49058  nnpw2blen  49076  blennngt2o2  49088  blennn0e2  49090  dignn0ldlem  49098  line  49228  rrxline  49230  aacllem  50296