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 3898	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4576	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2982	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 575	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 274	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   ∈ wcel 2107   ≠ wne 2944   ∖ cdif 3885  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-v 3435  df-dif 3891  df-sn 4563

This theorem is referenced by:  elpwdifsn  4723  eldifsni  4724  rexdifsn  4728  raldifsni  4729  eldifvsn  4731  difsn  4732  prproe  4838  sossfld  6094  tpres  7085  onmindif2  7666  mptsuppd  8012  suppssr  8021  suppssov1  8023  suppsssn  8026  suppssfv  8027  dif1o  8339  difsnen  8849  limenpsi  8948  frfi  9068  fofinf1o  9103  en2eleq  9773  en2other2  9774  dfac8clem  9797  acni2  9811  acndom  9816  acnnum  9817  dfac9  9901  dfacacn  9906  kmlem3  9917  kmlem4  9918  fin23lem21  10104  canthp1lem2  10418  elni  10641  mulnzcnopr  11630  divval  11644  elnnne0  12256  elq  12699  rpcndif0  12758  modfzo0difsn  13672  modsumfzodifsn  13673  expcl2lem  13803  expclzlem  13815  hashdifpr  14139  hashgt23el  14148  prprrab  14196  hashle2prv  14201  reccn2  15315  rlimdiv  15366  eff2  15817  tanval  15846  rpnnen2lem9  15940  fzo0dvdseq  16041  oddprmgt2  16413  oddprmdvds  16613  4sqlem19  16673  prmlem0  16816  prmlem1a  16817  setsnid  16919  setsnidOLD  16920  grpinvnzcl  18656  symgextf  19034  f1omvdmvd  19060  pmtrprfv  19070  odcau  19218  efgsf  19344  efgsrel  19349  efgs1  19350  efgs1b  19351  efgsp1  19352  efgsres  19353  efgredlema  19355  efgredlemd  19359  efgrelexlemb  19365  gsumpt  19572  dmdprdd  19611  dprdcntz  19620  dprdfeq0  19634  dprd2da  19654  drngunit  20005  isdrng2  20010  drngid2  20016  isdrngd  20025  issubdrg  20058  sdrgacs  20078  cntzsdrg  20079  abvtriv  20110  islss  20205  lssneln0  20223  lssssr  20224  lbsind  20351  lbspss  20353  lspabs3  20392  lspsneq  20393  lspfixed  20399  lspexch  20400  islbs2  20425  isdomn2  20579  domnrrg  20580  cnflddiv  20637  cnfldinv  20638  xrs1mnd  20645  xrs10  20646  xrge0subm  20648  cnsubdrglem  20658  cnmgpid  20669  cnmsubglem  20670  gzrngunit  20673  zringunit  20697  zringndrg  20699  domnchr  20745  cnmsgngrp  20793  psgninv  20796  psgndiflemB  20814  lindfind  21032  lindsind  21033  lindff1  21036  lindfrn  21037  mvrcl  21230  coe1tmmul2  21456  mdetunilem9  21778  maducoeval2  21798  gsummatr01lem4  21816  ist1-2  22507  cmpfi  22568  2ndcdisj  22616  2ndcsep  22619  locfincmp  22686  alexsublem  23204  cldsubg  23271  imasdsf1olem  23535  prdsxmslem2  23694  reperflem  23990  xrge0gsumle  24005  xrge0tsms  24006  divcn  24040  evth  24131  cvsdiv  24304  cvsdivcl  24305  cphreccllem  24351  bcthlem5  24501  itg11  24864  i1fmullem  24867  i1fadd  24868  itg1addlem2  24870  i1fmulc  24877  itg1mulc  24878  ellimc3  25052  limcmpt2  25057  dvlem  25069  dvidlem  25088  dvcnp  25092  dvcobr  25119  dvrec  25128  dvrecg  25146  dvmptdiv  25147  dvcnvlem  25149  dvexp3  25151  dveflem  25152  dvferm1lem  25157  dvferm2lem  25159  lhop1lem  25186  ftc1lem5  25213  mdegleb  25238  coe1mul3  25273  ply1nz  25295  fta1blem  25342  fta1b  25343  ig1peu  25345  ig1pdvds  25350  plyeq0lem  25380  dgrub  25404  quotval  25461  fta1lem  25476  fta1  25477  elqaalem3  25490  qaa  25492  iaa  25494  aareccl  25495  aannenlem2  25498  abelthlem8  25607  abelth  25609  eff1olem  25713  logrncl  25732  eflog  25741  logeftb  25748  logdmss  25806  dvlog  25815  logbcl  25926  logbid1  25927  logb1  25928  elogb  25929  logbchbase  25930  relogbval  25931  relogbcl  25932  relogbreexp  25934  relogbmul  25936  nnlogbexp  25940  relogbcxp  25944  cxplogb  25945  relogbcxpb  25946  logbf  25948  logblog  25951  2logb9irrALT  25957  sqrt2cxp2logb9e3  25958  angval  25960  dcubic  26005  rlimcnp  26124  efrlim  26128  logexprlim  26382  dchrghm  26413  dchrabs  26417  lgsfcl2  26460  lgsval2lem  26464  lgsval3  26472  lgsmod  26480  lgsdirprm  26488  lgsne0  26492  gausslemma2dlem0f  26518  lgsquad2lem2  26542  2lgsoddprm  26573  2sqlem11  26586  2sqblem  26588  dchrvmaeq0  26661  rpvmasum2  26669  dchrisum0re  26670  qrngdiv  26781  tglngval  26921  tgisline  26997  axlowdimlem9  27327  axlowdimlem12  27330  axlowdimlem13  27331  elntg2  27362  upgrbi  27472  upgr1elem  27491  umgrislfupgrlem  27501  edgupgr  27513  subgruhgredgd  27660  upgrreslem  27680  nbgrel  27716  nbupgr  27720  nbupgrel  27721  nbumgrvtx  27722  nbgrssovtx  27737  nbupgrres  27740  nbusgrvtxm1uvtx  27781  nbupgruvtxres  27783  iscplgredg  27793  cusgredg  27800  cusgrfilem2  27832  usgredgsscusgredg  27835  1loopgrnb0  27878  1egrvtxdg0  27887  uhgrvd00  27910  vtxdginducedm1lem4  27918  eupth2lem3lem3  28603  frcond1  28639  frcond4  28643  2pthfrgr  28657  3cyclfrgrrn1  28658  n4cyclfrgr  28664  frgrwopreglem4a  28683  numclwwlk5  28761  ressupprn  31033  suppss3  31068  xdivval  31202  xrge0tsmsd  31326  pmtrcnel  31367  pmtrcnelor  31369  0nellinds  31575  extdg1id  31747  submatminr1  31769  ordtconnlem1  31883  ispisys2  32130  sigapisys  32132  sibfinima  32315  sseqf  32368  signswch  32549  signstfvn  32557  signsvtn0  32558  signstfvneq0  32560  signstfvcl  32561  signstfveq0a  32564  signstfveq0  32565  signsvfn  32570  signsvtp  32571  signsvtn  32572  signsvfpn  32573  signsvfnn  32574  signlem0  32575  bnj158  32717  bnj168  32718  bnj529  32730  bnj906  32919  bnj970  32936  exdifsn  33062  cusgredgex2  33093  subfacp1lem5  33155  cvmsi  33236  cvmsval  33237  cvmsdisj  33241  cvmscld  33244  cvmsss2  33245  satfv1lem  33333  sinccvglem  33639  circum  33641  xpord3ind  33809  addsval  34135  unbdqndv2lem2  34699  bj-0int  35281  lindsadd  35779  lindsenlbs  35781  matunitlindflem2  35783  matunitlindf  35784  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem16  35802  poimirlem18  35804  poimirlem19  35805  poimirlem21  35807  poimirlem22  35808  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  itg2addnclem2  35838  sdclem1  35910  rrncmslem  35999  rrnequiv  36002  isdrngo2  36125  isdrngo3  36126  prtlem100  36880  prter2  36902  prter3  36903  lsatlspsn2  37013  lsateln0  37016  lsatn0  37020  lsatspn0  37021  lsatcmp  37024  lsatelbN  37027  islshpat  37038  lsat0cv  37054  lkrlspeqN  37192  dvheveccl  39133  dihlatat  39358  dochnel  39414  dihjat1  39450  dvh4dimlem  39464  dochsnkr2cl  39495  dochkr1  39499  dochkr1OLDN  39500  lcfl6lem  39519  lcfl9a  39526  lclkrlem2l  39539  lclkrlem2o  39542  lclkrlem2q  39544  lcfrlem9  39571  lcfrlem16  39579  lcfrlem17  39580  lcfrlem27  39590  lcfrlem37  39600  lcfrlem38  39601  lcfrlem40  39603  lcdlkreqN  39643  mapdrvallem2  39666  mapdn0  39690  mapdpglem20  39712  mapdpglem30  39723  mapdindp0  39740  mapdhcl  39748  mapdh6aN  39756  mapdh6dN  39760  mapdh6eN  39761  mapdh6kN  39767  mapdh8  39809  hdmap1l6a  39830  hdmap1l6d  39834  hdmap1l6e  39835  hdmap1l6k  39841  hdmapval3N  39859  hdmap10  39861  hdmap11lem2  39863  hdmapnzcl  39866  hdmaprnlem3eN  39879  hdmaprnlem17N  39884  hdmap14lem4a  39892  hdmap14lem7  39895  hdmap14lem14  39902  hgmaprnlem5N  39921  hdmaplkr  39934  hdmapip0  39936  hgmapvvlem2  39945  hgmapvvlem3  39946  hgmapvv  39947  fsuppind  40286  0prjspnlem  40467  pellexlem5  40662  dfac11  40894  dfacbasgrp  40940  dgraalem  40977  dgraaub  40980  aaitgo  40994  proot1ex  41033  isdomn3  41036  deg1mhm  41039  ofdivrec  41951  ofdivcan4  41952  ofdivdiv2  41953  expgrowth  41960  binomcxplemnotnn0  41981  dvdivbd  43471  dvdivcncf  43475  dirkeritg  43650  fourierdlem39  43694  fourierdlem57  43711  fourierdlem58  43712  fourierdlem59  43713  fourierdlem68  43722  fourierdlem76  43730  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  setsnidel  44840  sprvalpwn0  44946  odz2prm2pw  45026  fmtnoprmfac1  45028  fmtnoprmfac2  45030  sfprmdvdsmersenne  45066  lighneallem2  45069  lighneallem3  45070  lighneal  45074  oddprmALTV  45150  evenprm2  45177  oddprmne2  45178  odd2prm2  45181  even3prm2  45182  2zrngnmrid  45519  lincext1  45806  lindslinindsimp2lem5  45814  rege1logbrege0  45915  fllogbd  45917  relogbmulbexp  45918  relogbdivb  45919  nnpw2blen  45937  blennngt2o2  45949  blennn0e2  45951  dignn0ldlem  45959  line  46089  rrxline  46091  aacllem  46516