Theorem eldifsn 4744

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 3913	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4596	. . . 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 3900  {csn 4582

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 3444  df-dif 3906  df-sn 4583

This theorem is referenced by:  eldifsnd  4745  elpwdifsn  4747  eldifsni  4748  rexdifsn  4752  raldifsni  4753  eldifvsn  4755  difsn  4756  sossfld  6154  tpres  7159  onmindif2  7764  xpord3pred  8106  xpord3inddlem  8108  mptsuppd  8141  suppssr  8149  suppssov1  8151  suppssov2  8152  suppsssn  8155  suppssfv  8156  dif1o  8439  difsnen  9001  limenpsi  9094  frfi  9199  fofinf1o  9246  en2eleq  9932  en2other2  9933  dfac8clem  9956  acni2  9970  acndom  9975  acnnum  9976  dfac9  10061  dfacacn  10066  kmlem3  10077  kmlem4  10078  fin23lem21  10263  canthp1lem2  10578  elni  10801  mulnzcnf  11797  divval  11812  elnnne0  12429  elq  12877  rpcndif0  12940  modfzo0difsn  13880  modsumfzodifsn  13881  expcl2lem  14010  expclzlem  14020  hashdifpr  14352  hashgt23el  14361  prprrab  14410  hashle2prv  14415  reccn2  15534  rlimdiv  15583  eff2  16038  tanval  16067  rpnnen2lem9  16161  fzo0dvdseq  16264  oddprmgt2  16640  oddprmdvds  16845  4sqlem19  16905  prmlem0  17047  prmlem1a  17048  setsnid  17149  grpinvnzcl  18958  symgextf  19363  f1omvdmvd  19389  pmtrprfv  19399  odcau  19550  efgsf  19675  efgsrel  19680  efgs1  19681  efgs1b  19682  efgsp1  19683  efgsres  19684  efgredlema  19686  efgredlemd  19690  efgrelexlemb  19696  gsumpt  19908  dmdprdd  19947  dprdcntz  19956  dprdfeq0  19970  dprd2da  19990  isdomn2OLD  20662  domnrrg  20663  isdomn3  20665  drngunit  20684  isdrng2  20693  drngmcl  20700  drngid2  20702  isdrngd  20715  isdrngdOLD  20717  issubdrg  20730  sdrgacs  20751  cntzsdrg  20752  islss  20902  lssneln0  20921  lssssr  20922  lbsind  21049  lbspss  21051  lspabs3  21093  lspsneq  21094  lspfixed  21100  lspexch  21101  islbs2  21126  cnflddivOLD  21373  cnfldinv  21374  cnsubdrglem  21390  cnmgpid  21401  cnmsubglem  21402  gzrngunit  21405  xrs1mnd  21412  xrs10  21413  xrge0subm  21415  zringunit  21438  zringndrg  21440  domnchr  21504  cnmsgngrp  21551  psgninv  21554  psgndiflemB  21572  lindfind  21788  lindsind  21789  lindff1  21792  lindfrn  21793  mvrcl  21964  coe1tmmul2  22235  mdetunilem9  22581  maducoeval2  22601  gsummatr01lem4  22619  ist1-2  23308  cmpfi  23369  2ndcdisj  23417  2ndcsep  23420  locfincmp  23487  alexsublem  24005  cldsubg  24072  imasdsf1olem  24334  prdsxmslem2  24490  reperflem  24780  xrge0gsumle  24795  xrge0tsms  24796  divcnOLD  24830  divcn  24832  evth  24931  cvsdiv  25105  cvsdivcl  25106  cphreccllem  25151  bcthlem5  25301  itg11  25665  i1fmullem  25668  i1fadd  25669  itg1addlem2  25671  i1fmulc  25677  itg1mulc  25678  ellimc3  25853  limcmpt2  25858  dvlem  25870  dvidlem  25889  dvcnp  25893  dvcobr  25922  dvcobrOLD  25923  dvrec  25932  dvrecg  25950  dvmptdiv  25951  dvcnvlem  25953  dvexp3  25955  dveflem  25956  dvferm1lem  25961  dvferm2lem  25963  lhop1lem  25991  ftc1lem5  26020  mdegleb  26042  coe1mul3  26077  ply1nz  26100  fta1blem  26149  fta1b  26150  ig1peu  26153  ig1pdvds  26158  plyeq0lem  26188  dgrub  26212  quotval  26273  fta1lem  26288  fta1  26289  elqaalem3  26302  qaa  26304  iaa  26306  aareccl  26307  aannenlem2  26310  abelthlem8  26422  abelth  26424  eff1olem  26530  logrncl  26549  eflog  26558  logeftb  26565  logdmss  26624  dvlog  26633  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  27209  dchrghm  27240  dchrabs  27244  lgsfcl2  27287  lgsval2lem  27291  lgsval3  27299  lgsmod  27307  lgsdirprm  27315  lgsne0  27319  gausslemma2dlem0f  27345  lgsquad2lem2  27369  2lgsoddprm  27400  2sqlem11  27413  2sqblem  27415  dchrvmaeq0  27488  rpvmasum2  27496  dchrisum0re  27497  qrngdiv  27608  addsval  27975  divsval  28202  elnns  28353  1nns  28362  tglngval  28641  tgisline  28717  axlowdimlem9  29041  axlowdimlem12  29044  axlowdimlem13  29045  elntg2  29076  upgrbi  29184  upgr1elem  29203  umgrislfupgrlem  29213  edgupgr  29225  subgruhgredgd  29375  upgrreslem  29395  nbgrel  29431  nbupgr  29435  nbupgrel  29436  nbumgrvtx  29437  nbgrssovtx  29452  nbupgrres  29455  nbusgrvtxm1uvtx  29496  nbupgruvtxres  29498  iscplgredg  29508  cusgredg  29515  cusgrfilem2  29548  usgredgsscusgredg  29551  1loopgrnb0  29594  1egrvtxdg0  29603  uhgrvd00  29626  vtxdginducedm1lem4  29634  eupth2lem3lem3  30323  frcond1  30359  frcond4  30363  2pthfrgr  30377  3cyclfrgrrn1  30378  n4cyclfrgr  30384  frgrwopreglem4a  30403  numclwwlk5  30481  ressupprn  32786  suppss3  32819  xdivval  33017  xrge0tsmsd  33173  pmtrcnel  33189  pmtrcnelor  33191  0nellinds  33469  dvdsruasso  33484  mxidlirredi  33570  extdg1id  33850  irngnzply1  33875  submatminr1  33994  ordtconnlem1  34108  ispisys2  34337  sigapisys  34339  sibfinima  34523  sseqf  34576  signswch  34745  signstfvn  34753  signsvtn0  34754  signstfvneq0  34756  signstfvcl  34757  signstfveq0a  34760  signstfveq0  34761  signsvfn  34766  signsvtp  34767  signsvtn  34768  signsvfpn  34769  signsvfnn  34770  signlem0  34771  bnj158  34912  bnj168  34913  bnj529  34924  bnj906  35112  bnj970  35129  exdifsn  35261  cusgredgex2  35345  subfacp1lem5  35406  cvmsi  35487  cvmsval  35488  cvmsdisj  35492  cvmscld  35495  cvmsss2  35496  satfv1lem  35584  sinccvglem  35894  circum  35896  mpomulnzcnf  36521  unbdqndv2lem2  36738  bj-0int  37381  lindsadd  37893  lindsenlbs  37895  matunitlindflem2  37897  matunitlindf  37898  poimirlem6  37906  poimirlem7  37907  poimirlem8  37908  poimirlem16  37916  poimirlem18  37918  poimirlem19  37919  poimirlem21  37921  poimirlem22  37922  poimirlem24  37924  poimirlem25  37925  poimirlem26  37926  poimirlem27  37927  itg2addnclem2  37952  sdclem1  38023  rrncmslem  38112  rrnequiv  38115  isdrngo2  38238  isdrngo3  38239  eldmxrncnvepres  38714  eldmxrncnvepres2  38715  prtlem100  39264  prter2  39286  prter3  39287  lsatlspsn2  39397  lsateln0  39400  lsatn0  39404  lsatspn0  39405  lsatcmp  39408  lsatelbN  39411  islshpat  39422  lsat0cv  39438  lkrlspeqN  39576  dvheveccl  41517  dihlatat  41742  dochnel  41798  dihjat1  41834  dvh4dimlem  41848  dochsnkr2cl  41879  dochkr1  41883  dochkr1OLDN  41884  lcfl6lem  41903  lcfl9a  41910  lclkrlem2l  41923  lclkrlem2o  41926  lclkrlem2q  41928  lcfrlem9  41955  lcfrlem16  41963  lcfrlem17  41964  lcfrlem27  41974  lcfrlem37  41984  lcfrlem38  41985  lcfrlem40  41987  lcdlkreqN  42027  mapdrvallem2  42050  mapdn0  42074  mapdpglem20  42096  mapdpglem30  42107  mapdindp0  42124  mapdhcl  42132  mapdh6aN  42140  mapdh6dN  42144  mapdh6eN  42145  mapdh6kN  42151  mapdh8  42193  hdmap1l6a  42214  hdmap1l6d  42218  hdmap1l6e  42219  hdmap1l6k  42225  hdmapval3N  42243  hdmap10  42245  hdmap11lem2  42247  hdmapnzcl  42250  hdmaprnlem3eN  42263  hdmaprnlem17N  42268  hdmap14lem4a  42276  hdmap14lem7  42279  hdmap14lem14  42286  hgmaprnlem5N  42305  hdmaplkr  42318  hdmapip0  42320  hgmapvvlem2  42329  hgmapvvlem3  42330  hgmapvv  42331  redvmptabs  42759  readvrec2  42760  readvrec  42761  fiabv  42935  fsuppind  42977  0prjspnlem  43010  pellexlem5  43219  dfac11  43448  dfacbasgrp  43494  dgraalem  43531  dgraaub  43534  aaitgo  43548  proot1ex  43582  deg1mhm  43586  ofdivrec  44711  ofdivcan4  44712  ofdivdiv2  44713  expgrowth  44720  binomcxplemnotnn0  44741  dvdivbd  46310  dvdivcncf  46314  dirkeritg  46489  fourierdlem39  46533  fourierdlem57  46550  fourierdlem58  46551  fourierdlem59  46552  fourierdlem68  46561  fourierdlem76  46569  fourierdlem103  46596  fourierdlem104  46597  fourierdlem111  46604  setsnidel  47766  sprvalpwn0  47872  odz2prm2pw  47952  fmtnoprmfac1  47954  fmtnoprmfac2  47956  sfprmdvdsmersenne  47992  lighneallem2  47995  lighneallem3  47996  lighneal  48000  oddprmALTV  48076  evenprm2  48103  oddprmne2  48104  odd2prm2  48107  even3prm2  48108  isubgruhgr  48257  grimuhgr  48276  2zrngnmrid  48645  lincext1  48843  lindslinindsimp2lem5  48851  rege1logbrege0  48947  fllogbd  48949  relogbmulbexp  48950  relogbdivb  48951  nnpw2blen  48969  blennngt2o2  48981  blennn0e2  48983  dignn0ldlem  48991  line  49121  rrxline  49123  aacllem  50189