Theorem eldifsn 4677

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 3868	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4536	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2988	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 578	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 278	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∈ wcel 2111   ≠ wne 2951   ∖ cdif 3855  {csn 4522

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ne 2952  df-v 3411  df-dif 3861  df-sn 4523

This theorem is referenced by:  elpwdifsn  4679  eldifsni  4680  rexdifsn  4684  raldifsni  4685  eldifvsn  4687  difsn  4688  prproe  4796  sossfld  6015  tpres  6954  onmindif2  7526  mptsuppd  7861  suppssr  7870  suppssov1  7872  suppsssn  7875  suppssfv  7876  dif1o  8135  difsnen  8620  limenpsi  8714  frfi  8796  fofinf1o  8832  en2eleq  9468  en2other2  9469  dfac8clem  9492  acni2  9506  acndom  9511  acnnum  9512  dfac9  9596  dfacacn  9601  kmlem3  9612  kmlem4  9613  fin23lem21  9799  canthp1lem2  10113  elni  10336  mulnzcnopr  11324  divval  11338  elnnne0  11948  elq  12390  rpcndif0  12449  modfzo0difsn  13360  modsumfzodifsn  13361  expcl2lem  13491  expclzlem  13503  hashdifpr  13826  hashgt23el  13835  prprrab  13883  hashle2prv  13888  reccn2  15001  rlimdiv  15050  eff2  15500  tanval  15529  rpnnen2lem9  15623  fzo0dvdseq  15724  oddprmgt2  16095  oddprmdvds  16294  4sqlem19  16354  prmlem0  16497  prmlem1a  16498  setsnid  16597  grpinvnzcl  18238  symgextf  18612  f1omvdmvd  18638  pmtrprfv  18648  odcau  18796  efgsf  18922  efgsrel  18927  efgs1  18928  efgs1b  18929  efgsp1  18930  efgsres  18931  efgredlema  18933  efgredlemd  18937  efgrelexlemb  18943  gsumpt  19150  dmdprdd  19189  dprdcntz  19198  dprdfeq0  19212  dprd2da  19232  drngunit  19575  isdrng2  19580  drngid2  19586  isdrngd  19595  issubdrg  19628  sdrgacs  19648  cntzsdrg  19649  abvtriv  19680  islss  19774  lssneln0  19792  lssssr  19793  lbsind  19920  lbspss  19922  lspabs3  19961  lspsneq  19962  lspfixed  19968  lspexch  19969  islbs2  19994  isdomn2  20140  domnrrg  20141  cnflddiv  20196  cnfldinv  20197  xrs1mnd  20204  xrs10  20205  xrge0subm  20207  cnsubdrglem  20217  cnmgpid  20228  cnmsubglem  20229  gzrngunit  20232  zringunit  20256  zringndrg  20258  domnchr  20300  cnmsgngrp  20344  psgninv  20347  psgndiflemB  20365  lindfind  20581  lindsind  20582  lindff1  20585  lindfrn  20586  mvrcl  20780  coe1tmmul2  21000  mdetunilem9  21320  maducoeval2  21340  gsummatr01lem4  21358  ist1-2  22047  cmpfi  22108  2ndcdisj  22156  2ndcsep  22159  locfincmp  22226  alexsublem  22744  cldsubg  22811  imasdsf1olem  23075  prdsxmslem2  23231  reperflem  23519  xrge0gsumle  23534  xrge0tsms  23535  divcn  23569  evth  23660  cvsdiv  23833  cvsdivcl  23834  cphreccllem  23879  bcthlem5  24028  itg11  24391  i1fmullem  24394  i1fadd  24395  itg1addlem2  24397  i1fmulc  24403  itg1mulc  24404  ellimc3  24578  limcmpt2  24583  dvlem  24595  dvidlem  24614  dvcnp  24618  dvcobr  24645  dvrec  24654  dvrecg  24672  dvmptdiv  24673  dvcnvlem  24675  dvexp3  24677  dveflem  24678  dvferm1lem  24683  dvferm2lem  24685  lhop1lem  24712  ftc1lem5  24739  mdegleb  24764  coe1mul3  24799  ply1nz  24821  fta1blem  24868  fta1b  24869  ig1peu  24871  ig1pdvds  24876  plyeq0lem  24906  dgrub  24930  quotval  24987  fta1lem  25002  fta1  25003  elqaalem3  25016  qaa  25018  iaa  25020  aareccl  25021  aannenlem2  25024  abelthlem8  25133  abelth  25135  eff1olem  25239  logrncl  25258  eflog  25267  logeftb  25274  logdmss  25332  dvlog  25341  logbcl  25452  logbid1  25453  logb1  25454  elogb  25455  logbchbase  25456  relogbval  25457  relogbcl  25458  relogbreexp  25460  relogbmul  25462  nnlogbexp  25466  relogbcxp  25470  cxplogb  25471  relogbcxpb  25472  logbf  25474  logblog  25477  2logb9irrALT  25483  sqrt2cxp2logb9e3  25484  angval  25486  dcubic  25531  rlimcnp  25650  efrlim  25654  logexprlim  25908  dchrghm  25939  dchrabs  25943  lgsfcl2  25986  lgsval2lem  25990  lgsval3  25998  lgsmod  26006  lgsdirprm  26014  lgsne0  26018  gausslemma2dlem0f  26044  lgsquad2lem2  26068  2lgsoddprm  26099  2sqlem11  26112  2sqblem  26114  dchrvmaeq0  26187  rpvmasum2  26195  dchrisum0re  26196  qrngdiv  26307  tglngval  26444  tgisline  26520  axlowdimlem9  26843  axlowdimlem12  26846  axlowdimlem13  26847  elntg2  26878  upgrbi  26985  upgr1elem  27004  umgrislfupgrlem  27014  edgupgr  27026  subgruhgredgd  27173  upgrreslem  27193  nbgrel  27229  nbupgr  27233  nbupgrel  27234  nbumgrvtx  27235  nbgrssovtx  27250  nbupgrres  27253  nbusgrvtxm1uvtx  27294  nbupgruvtxres  27296  iscplgredg  27306  cusgredg  27313  cusgrfilem2  27345  usgredgsscusgredg  27348  1loopgrnb0  27391  1egrvtxdg0  27400  uhgrvd00  27423  vtxdginducedm1lem4  27431  eupth2lem3lem3  28114  frcond1  28150  frcond4  28154  2pthfrgr  28168  3cyclfrgrrn1  28169  n4cyclfrgr  28175  frgrwopreglem4a  28194  numclwwlk5  28272  ressupprn  30548  suppss3  30583  xdivval  30717  xrge0tsmsd  30843  pmtrcnel  30884  pmtrcnelor  30886  0nellinds  31087  extdg1id  31259  submatminr1  31281  ordtconnlem1  31395  ispisys2  31640  sigapisys  31642  sibfinima  31825  sseqf  31878  signswch  32059  signstfvn  32067  signsvtn0  32068  signstfvneq0  32070  signstfvcl  32071  signstfveq0a  32074  signstfveq0  32075  signsvfn  32080  signsvtp  32081  signsvtn  32082  signsvfpn  32083  signsvfnn  32084  signlem0  32085  bnj158  32227  bnj168  32228  bnj529  32240  bnj906  32430  bnj970  32447  exdifsn  32573  cusgredgex2  32600  subfacp1lem5  32662  cvmsi  32743  cvmsval  32744  cvmsdisj  32748  cvmscld  32751  cvmsss2  32752  satfv1lem  32840  sinccvglem  33146  circum  33148  unbdqndv2lem2  34239  bj-0int  34796  lindsadd  35330  lindsenlbs  35332  matunitlindflem2  35334  matunitlindf  35335  poimirlem6  35343  poimirlem7  35344  poimirlem8  35345  poimirlem16  35353  poimirlem18  35355  poimirlem19  35356  poimirlem21  35358  poimirlem22  35359  poimirlem24  35361  poimirlem25  35362  poimirlem26  35363  poimirlem27  35364  itg2addnclem2  35389  sdclem1  35461  rrncmslem  35550  rrnequiv  35553  isdrngo2  35676  isdrngo3  35677  prtlem100  36435  prter2  36457  prter3  36458  lsatlspsn2  36568  lsateln0  36571  lsatn0  36575  lsatspn0  36576  lsatcmp  36579  lsatelbN  36582  islshpat  36593  lsat0cv  36609  lkrlspeqN  36747  dvheveccl  38688  dihlatat  38913  dochnel  38969  dihjat1  39005  dvh4dimlem  39019  dochsnkr2cl  39050  dochkr1  39054  dochkr1OLDN  39055  lcfl6lem  39074  lcfl9a  39081  lclkrlem2l  39094  lclkrlem2o  39097  lclkrlem2q  39099  lcfrlem9  39126  lcfrlem16  39134  lcfrlem17  39135  lcfrlem27  39145  lcfrlem37  39155  lcfrlem38  39156  lcfrlem40  39158  lcdlkreqN  39198  mapdrvallem2  39221  mapdn0  39245  mapdpglem20  39267  mapdpglem30  39278  mapdindp0  39295  mapdhcl  39303  mapdh6aN  39311  mapdh6dN  39315  mapdh6eN  39316  mapdh6kN  39322  mapdh8  39364  hdmap1l6a  39385  hdmap1l6d  39389  hdmap1l6e  39390  hdmap1l6k  39396  hdmapval3N  39414  hdmap10  39416  hdmap11lem2  39418  hdmapnzcl  39421  hdmaprnlem3eN  39434  hdmaprnlem17N  39439  hdmap14lem4a  39447  hdmap14lem7  39450  hdmap14lem14  39457  hgmaprnlem5N  39476  hdmaplkr  39489  hdmapip0  39491  hgmapvvlem2  39500  hgmapvvlem3  39501  hgmapvv  39502  fsuppind  39784  0prjspnlem  39957  pellexlem5  40147  dfac11  40379  dfacbasgrp  40425  dgraalem  40462  dgraaub  40465  aaitgo  40479  proot1ex  40518  isdomn3  40521  deg1mhm  40524  ofdivrec  41403  ofdivcan4  41404  ofdivdiv2  41405  expgrowth  41412  binomcxplemnotnn0  41433  dvdivbd  42931  dvdivcncf  42935  dirkeritg  43110  fourierdlem39  43154  fourierdlem57  43171  fourierdlem58  43172  fourierdlem59  43173  fourierdlem68  43182  fourierdlem76  43190  fourierdlem103  43217  fourierdlem104  43218  fourierdlem111  43225  setsnidel  44262  sprvalpwn0  44368  odz2prm2pw  44448  fmtnoprmfac1  44450  fmtnoprmfac2  44452  sfprmdvdsmersenne  44488  lighneallem2  44491  lighneallem3  44492  lighneal  44496  oddprmALTV  44572  evenprm2  44599  oddprmne2  44600  odd2prm2  44603  even3prm2  44604  2zrngnmrid  44941  lincext1  45228  lindslinindsimp2lem5  45236  rege1logbrege0  45337  fllogbd  45339  relogbmulbexp  45340  relogbdivb  45341  nnpw2blen  45359  blennngt2o2  45371  blennn0e2  45373  dignn0ldlem  45381  line  45511  rrxline  45513  aacllem  45720