Theorem eldifsn 4721

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 3895	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4571	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2967	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 574	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 275	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   ≠ wne 2930   ∖ cdif 3882  {csn 4557

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ne 2931  df-v 3429  df-dif 3888  df-sn 4558

This theorem is referenced by:  eldifsnd  4722  eldifsni  4725  rexdifsn  4729  raldifsni  4730  eldifvsn  4732  difsn  4733  sossfld  6139  tpres  7145  onmindif2  7750  xpord3pred  8091  xpord3inddlem  8093  mptsuppd  8126  suppssr  8134  suppssov1  8136  suppssov2  8137  suppsssn  8140  suppssfv  8141  dif1o  8424  difsnen  8986  limenpsi  9079  frfi  9184  fofinf1o  9231  en2eleq  9919  en2other2  9920  dfac8clem  9943  acni2  9957  acndom  9962  acnnum  9963  dfac9  10048  dfacacn  10053  kmlem3  10064  kmlem4  10065  fin23lem21  10250  canthp1lem2  10565  elni  10788  mulnzcnf  11785  divval  11800  elnnne0  12440  elq  12889  rpcndif0  12952  modfzo0difsn  13894  modsumfzodifsn  13895  expcl2lem  14024  expclzlem  14034  hashdifpr  14366  hashgt23el  14375  prprrab  14424  hashle2prv  14429  reccn2  15548  rlimdiv  15597  eff2  16055  tanval  16084  rpnnen2lem9  16178  fzo0dvdseq  16281  oddprmgt2  16658  oddprmdvds  16863  4sqlem19  16923  prmlem0  17065  prmlem1a  17066  setsnid  17167  grpinvnzcl  18976  symgextf  19381  f1omvdmvd  19407  pmtrprfv  19417  odcau  19568  efgsf  19693  efgsrel  19698  efgs1  19699  efgs1b  19700  efgsp1  19701  efgsres  19702  efgredlema  19704  efgredlemd  19708  efgrelexlemb  19714  gsumpt  19926  dmdprdd  19965  dprdcntz  19974  dprdfeq0  19988  dprd2da  20008  isdomn2OLD  20678  domnrrg  20679  isdomn3  20681  drngunit  20700  isdrng2  20709  drngmcl  20716  drngid2  20718  isdrngd  20731  isdrngdOLD  20733  issubdrg  20746  sdrgacs  20767  cntzsdrg  20768  islss  20918  lssneln0  20937  lssssr  20938  lbsind  21064  lbspss  21066  lspabs3  21108  lspsneq  21109  lspfixed  21115  lspexch  21116  islbs2  21141  cnfldinv  21372  cnsubdrglem  21387  cnmgpid  21398  cnmsubglem  21399  gzrngunit  21402  xrs1mnd  21409  xrs10  21410  xrge0subm  21412  zringunit  21435  zringndrg  21437  domnchr  21501  cnmsgngrp  21548  psgninv  21551  psgndiflemB  21569  lindfind  21785  lindsind  21786  lindff1  21789  lindfrn  21790  mvrcl  21959  coe1tmmul2  22229  mdetunilem9  22573  maducoeval2  22593  gsummatr01lem4  22611  ist1-2  23300  cmpfi  23361  2ndcdisj  23409  2ndcsep  23412  locfincmp  23479  alexsublem  23997  cldsubg  24064  imasdsf1olem  24326  prdsxmslem2  24482  reperflem  24772  xrge0gsumle  24787  xrge0tsms  24788  divcn  24823  evth  24914  cvsdiv  25087  cvsdivcl  25088  cphreccllem  25133  bcthlem5  25283  itg11  25646  i1fmullem  25649  i1fadd  25650  itg1addlem2  25652  i1fmulc  25658  itg1mulc  25659  ellimc3  25834  limcmpt2  25839  dvlem  25851  dvidlem  25870  dvcnp  25874  dvcobr  25901  dvrec  25910  dvrecg  25928  dvmptdiv  25929  dvcnvlem  25931  dvexp3  25933  dveflem  25934  dvferm1lem  25939  dvferm2lem  25941  lhop1lem  25968  ftc1lem5  25995  mdegleb  26017  coe1mul3  26052  ply1nz  26075  fta1blem  26124  fta1b  26125  ig1peu  26128  ig1pdvds  26133  plyeq0lem  26163  dgrub  26187  quotval  26246  fta1lem  26261  fta1  26262  elqaalem3  26275  qaa  26277  iaa  26279  aareccl  26280  aannenlem2  26283  abelthlem8  26392  abelth  26394  eff1olem  26500  logrncl  26519  eflog  26528  logeftb  26535  logdmss  26594  dvlog  26603  logbcl  26719  logbid1  26720  logb1  26721  elogb  26722  logbchbase  26723  relogbval  26724  relogbcl  26725  relogbreexp  26727  relogbmul  26729  nnlogbexp  26733  relogbcxp  26737  cxplogb  26738  relogbcxpb  26739  logbf  26741  logblog  26744  2logb9irrALT  26750  sqrt2cxp2logb9e3  26751  angval  26753  dcubic  26798  rlimcnp  26917  efrlim  26921  logexprlim  27176  dchrghm  27207  dchrabs  27211  lgsfcl2  27254  lgsval2lem  27258  lgsval3  27266  lgsmod  27274  lgsdirprm  27282  lgsne0  27286  gausslemma2dlem0f  27312  lgsquad2lem2  27336  2lgsoddprm  27367  2sqlem11  27380  2sqblem  27382  dchrvmaeq0  27455  rpvmasum2  27463  dchrisum0re  27464  qrngdiv  27575  addsval  27942  divsval  28169  elnns  28320  1nns  28329  tglngval  28607  tgisline  28683  axlowdimlem9  29007  axlowdimlem12  29010  axlowdimlem13  29011  elntg2  29042  upgrbi  29150  upgr1elem  29169  umgrislfupgrlem  29179  edgupgr  29191  subgruhgredgd  29341  upgrreslem  29361  nbgrel  29397  nbupgr  29401  nbupgrel  29402  nbumgrvtx  29403  nbgrssovtx  29418  nbupgrres  29421  nbusgrvtxm1uvtx  29462  nbupgruvtxres  29464  iscplgredg  29474  cusgredg  29481  cusgrfilem2  29513  usgredgsscusgredg  29516  1loopgrnb0  29559  1egrvtxdg0  29568  uhgrvd00  29591  vtxdginducedm1lem4  29599  eupth2lem3lem3  30288  frcond1  30324  frcond4  30328  2pthfrgr  30342  3cyclfrgrrn1  30343  n4cyclfrgr  30349  frgrwopreglem4a  30368  numclwwlk5  30446  ressupprn  32751  suppss3  32784  xdivval  32966  xrge0tsmsd  33122  pmtrcnel  33138  pmtrcnelor  33140  0nellinds  33418  dvdsruasso  33433  mxidlirredi  33519  extdg1id  33798  irngnzply1  33823  submatminr1  33942  ordtconnlem1  34056  ispisys2  34285  sigapisys  34287  sibfinima  34471  sseqf  34524  signswch  34693  signstfvn  34701  signsvtn0  34702  signstfvneq0  34704  signstfvcl  34705  signstfveq0a  34708  signstfveq0  34709  signsvfn  34714  signsvtp  34715  signsvtn  34716  signsvfpn  34717  signsvfnn  34718  signlem0  34719  bnj158  34860  bnj168  34861  bnj529  34872  bnj906  35060  bnj970  35077  exdifsn  35209  cusgredgex2  35293  subfacp1lem5  35354  cvmsi  35435  cvmsval  35436  cvmsdisj  35440  cvmscld  35443  cvmsss2  35444  satfv1lem  35532  sinccvglem  35842  circum  35844  mpomulnzcnf  36469  unbdqndv2lem2  36758  bj-0int  37401  lindsadd  37922  lindsenlbs  37924  matunitlindflem2  37926  matunitlindf  37927  poimirlem6  37935  poimirlem7  37936  poimirlem8  37937  poimirlem16  37945  poimirlem18  37947  poimirlem19  37948  poimirlem21  37950  poimirlem22  37951  poimirlem24  37953  poimirlem25  37954  poimirlem26  37955  poimirlem27  37956  itg2addnclem2  37981  sdclem1  38052  rrncmslem  38141  rrnequiv  38144  isdrngo2  38267  isdrngo3  38268  eldmxrncnvepres  38743  eldmxrncnvepres2  38744  prtlem100  39293  prter2  39315  prter3  39316  lsatlspsn2  39426  lsateln0  39429  lsatn0  39433  lsatspn0  39434  lsatcmp  39437  lsatelbN  39440  islshpat  39451  lsat0cv  39467  lkrlspeqN  39605  dvheveccl  41546  dihlatat  41771  dochnel  41827  dihjat1  41863  dvh4dimlem  41877  dochsnkr2cl  41908  dochkr1  41912  dochkr1OLDN  41913  lcfl6lem  41932  lcfl9a  41939  lclkrlem2l  41952  lclkrlem2o  41955  lclkrlem2q  41957  lcfrlem9  41984  lcfrlem16  41992  lcfrlem17  41993  lcfrlem27  42003  lcfrlem37  42013  lcfrlem38  42014  lcfrlem40  42016  lcdlkreqN  42056  mapdrvallem2  42079  mapdn0  42103  mapdpglem20  42125  mapdpglem30  42136  mapdindp0  42153  mapdhcl  42161  mapdh6aN  42169  mapdh6dN  42173  mapdh6eN  42174  mapdh6kN  42180  mapdh8  42222  hdmap1l6a  42243  hdmap1l6d  42247  hdmap1l6e  42248  hdmap1l6k  42254  hdmapval3N  42272  hdmap10  42274  hdmap11lem2  42276  hdmapnzcl  42279  hdmaprnlem3eN  42292  hdmaprnlem17N  42297  hdmap14lem4a  42305  hdmap14lem7  42308  hdmap14lem14  42315  hgmaprnlem5N  42334  hdmaplkr  42347  hdmapip0  42349  hgmapvvlem2  42358  hgmapvvlem3  42359  hgmapvv  42360  redvmptabs  42780  readvrec2  42781  readvrec  42782  fiabv  42969  fsuppind  43011  0prjspnlem  43044  pellexlem5  43249  dfac11  43478  dfacbasgrp  43524  dgraalem  43561  dgraaub  43564  aaitgo  43578  proot1ex  43612  deg1mhm  43616  ofdivrec  44741  ofdivcan4  44742  ofdivdiv2  44743  expgrowth  44750  binomcxplemnotnn0  44771  dvdivbd  46339  dvdivcncf  46343  dirkeritg  46518  fourierdlem39  46562  fourierdlem57  46579  fourierdlem58  46580  fourierdlem59  46581  fourierdlem68  46590  fourierdlem76  46598  fourierdlem103  46625  fourierdlem104  46626  fourierdlem111  46633  setsnidel  47825  sprvalpwn0  47931  odz2prm2pw  48014  fmtnoprmfac1  48016  fmtnoprmfac2  48018  sfprmdvdsmersenne  48054  lighneallem2  48057  lighneallem3  48058  lighneal  48062  oddprmALTV  48151  evenprm2  48178  oddprmne2  48179  odd2prm2  48182  even3prm2  48183  isubgruhgr  48332  grimuhgr  48351  2zrngnmrid  48720  lincext1  48918  lindslinindsimp2lem5  48926  rege1logbrege0  49022  fllogbd  49024  relogbmulbexp  49025  relogbdivb  49026  nnpw2blen  49044  blennngt2o2  49056  blennn0e2  49058  dignn0ldlem  49066  line  49196  rrxline  49198  aacllem  50264