Theorem eldifsn 4743

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 3912	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4595	. . . 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 3899  {csn 4581

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 3443  df-dif 3905  df-sn 4582

This theorem is referenced by:  eldifsnd  4744  elpwdifsn  4746  eldifsni  4747  rexdifsn  4751  raldifsni  4752  eldifvsn  4754  difsn  4755  sossfld  6145  tpres  7149  onmindif2  7754  xpord3pred  8096  xpord3inddlem  8098  mptsuppd  8131  suppssr  8139  suppssov1  8141  suppssov2  8142  suppsssn  8145  suppssfv  8146  dif1o  8429  difsnen  8991  limenpsi  9084  frfi  9189  fofinf1o  9236  en2eleq  9922  en2other2  9923  dfac8clem  9946  acni2  9960  acndom  9965  acnnum  9966  dfac9  10051  dfacacn  10056  kmlem3  10067  kmlem4  10068  fin23lem21  10253  canthp1lem2  10568  elni  10791  mulnzcnf  11787  divval  11802  elnnne0  12419  elq  12867  rpcndif0  12930  modfzo0difsn  13870  modsumfzodifsn  13871  expcl2lem  14000  expclzlem  14010  hashdifpr  14342  hashgt23el  14351  prprrab  14400  hashle2prv  14405  reccn2  15524  rlimdiv  15573  eff2  16028  tanval  16057  rpnnen2lem9  16151  fzo0dvdseq  16254  oddprmgt2  16630  oddprmdvds  16835  4sqlem19  16895  prmlem0  17037  prmlem1a  17038  setsnid  17139  grpinvnzcl  18945  symgextf  19350  f1omvdmvd  19376  pmtrprfv  19386  odcau  19537  efgsf  19662  efgsrel  19667  efgs1  19668  efgs1b  19669  efgsp1  19670  efgsres  19671  efgredlema  19673  efgredlemd  19677  efgrelexlemb  19683  gsumpt  19895  dmdprdd  19934  dprdcntz  19943  dprdfeq0  19957  dprd2da  19977  isdomn2OLD  20649  domnrrg  20650  isdomn3  20652  drngunit  20671  isdrng2  20680  drngmcl  20687  drngid2  20689  isdrngd  20702  isdrngdOLD  20704  issubdrg  20717  sdrgacs  20738  cntzsdrg  20739  islss  20889  lssneln0  20908  lssssr  20909  lbsind  21036  lbspss  21038  lspabs3  21080  lspsneq  21081  lspfixed  21087  lspexch  21088  islbs2  21113  cnflddivOLD  21360  cnfldinv  21361  cnsubdrglem  21377  cnmgpid  21388  cnmsubglem  21389  gzrngunit  21392  xrs1mnd  21399  xrs10  21400  xrge0subm  21402  zringunit  21425  zringndrg  21427  domnchr  21491  cnmsgngrp  21538  psgninv  21541  psgndiflemB  21559  lindfind  21775  lindsind  21776  lindff1  21779  lindfrn  21780  mvrcl  21951  coe1tmmul2  22222  mdetunilem9  22568  maducoeval2  22588  gsummatr01lem4  22606  ist1-2  23295  cmpfi  23356  2ndcdisj  23404  2ndcsep  23407  locfincmp  23474  alexsublem  23992  cldsubg  24059  imasdsf1olem  24321  prdsxmslem2  24477  reperflem  24767  xrge0gsumle  24782  xrge0tsms  24783  divcnOLD  24817  divcn  24819  evth  24918  cvsdiv  25092  cvsdivcl  25093  cphreccllem  25138  bcthlem5  25288  itg11  25652  i1fmullem  25655  i1fadd  25656  itg1addlem2  25658  i1fmulc  25664  itg1mulc  25665  ellimc3  25840  limcmpt2  25845  dvlem  25857  dvidlem  25876  dvcnp  25880  dvcobr  25909  dvcobrOLD  25910  dvrec  25919  dvrecg  25937  dvmptdiv  25938  dvcnvlem  25940  dvexp3  25942  dveflem  25943  dvferm1lem  25948  dvferm2lem  25950  lhop1lem  25978  ftc1lem5  26007  mdegleb  26029  coe1mul3  26064  ply1nz  26087  fta1blem  26136  fta1b  26137  ig1peu  26140  ig1pdvds  26145  plyeq0lem  26175  dgrub  26199  quotval  26260  fta1lem  26275  fta1  26276  elqaalem3  26289  qaa  26291  iaa  26293  aareccl  26294  aannenlem2  26297  abelthlem8  26409  abelth  26411  eff1olem  26517  logrncl  26536  eflog  26545  logeftb  26552  logdmss  26611  dvlog  26620  logbcl  26737  logbid1  26738  logb1  26739  elogb  26740  logbchbase  26741  relogbval  26742  relogbcl  26743  relogbreexp  26745  relogbmul  26747  nnlogbexp  26751  relogbcxp  26755  cxplogb  26756  relogbcxpb  26757  logbf  26759  logblog  26762  2logb9irrALT  26768  sqrt2cxp2logb9e3  26769  angval  26771  dcubic  26816  rlimcnp  26935  efrlim  26939  efrlimOLD  26940  logexprlim  27196  dchrghm  27227  dchrabs  27231  lgsfcl2  27274  lgsval2lem  27278  lgsval3  27286  lgsmod  27294  lgsdirprm  27302  lgsne0  27306  gausslemma2dlem0f  27332  lgsquad2lem2  27356  2lgsoddprm  27387  2sqlem11  27400  2sqblem  27402  dchrvmaeq0  27475  rpvmasum2  27483  dchrisum0re  27484  qrngdiv  27595  addsval  27962  divsval  28189  elnns  28340  1nns  28349  tglngval  28627  tgisline  28703  axlowdimlem9  29027  axlowdimlem12  29030  axlowdimlem13  29031  elntg2  29062  upgrbi  29170  upgr1elem  29189  umgrislfupgrlem  29199  edgupgr  29211  subgruhgredgd  29361  upgrreslem  29381  nbgrel  29417  nbupgr  29421  nbupgrel  29422  nbumgrvtx  29423  nbgrssovtx  29438  nbupgrres  29441  nbusgrvtxm1uvtx  29482  nbupgruvtxres  29484  iscplgredg  29494  cusgredg  29501  cusgrfilem2  29534  usgredgsscusgredg  29537  1loopgrnb0  29580  1egrvtxdg0  29589  uhgrvd00  29612  vtxdginducedm1lem4  29620  eupth2lem3lem3  30309  frcond1  30345  frcond4  30349  2pthfrgr  30363  3cyclfrgrrn1  30364  n4cyclfrgr  30370  frgrwopreglem4a  30389  numclwwlk5  30467  ressupprn  32771  suppss3  32804  xdivval  33002  xrge0tsmsd  33157  pmtrcnel  33173  pmtrcnelor  33175  0nellinds  33453  dvdsruasso  33468  mxidlirredi  33554  extdg1id  33825  irngnzply1  33850  submatminr1  33969  ordtconnlem1  34083  ispisys2  34312  sigapisys  34314  sibfinima  34498  sseqf  34551  signswch  34720  signstfvn  34728  signsvtn0  34729  signstfvneq0  34731  signstfvcl  34732  signstfveq0a  34735  signstfveq0  34736  signsvfn  34741  signsvtp  34742  signsvtn  34743  signsvfpn  34744  signsvfnn  34745  signlem0  34746  bnj158  34887  bnj168  34888  bnj529  34899  bnj906  35088  bnj970  35105  exdifsn  35237  cusgredgex2  35319  subfacp1lem5  35380  cvmsi  35461  cvmsval  35462  cvmsdisj  35466  cvmscld  35469  cvmsss2  35470  satfv1lem  35558  sinccvglem  35868  circum  35870  mpomulnzcnf  36495  unbdqndv2lem2  36712  bj-0int  37308  lindsadd  37816  lindsenlbs  37818  matunitlindflem2  37820  matunitlindf  37821  poimirlem6  37829  poimirlem7  37830  poimirlem8  37831  poimirlem16  37839  poimirlem18  37841  poimirlem19  37842  poimirlem21  37844  poimirlem22  37845  poimirlem24  37847  poimirlem25  37848  poimirlem26  37849  poimirlem27  37850  itg2addnclem2  37875  sdclem1  37946  rrncmslem  38035  rrnequiv  38038  isdrngo2  38161  isdrngo3  38162  eldmxrncnvepres  38637  eldmxrncnvepres2  38638  prtlem100  39187  prter2  39209  prter3  39210  lsatlspsn2  39320  lsateln0  39323  lsatn0  39327  lsatspn0  39328  lsatcmp  39331  lsatelbN  39334  islshpat  39345  lsat0cv  39361  lkrlspeqN  39499  dvheveccl  41440  dihlatat  41665  dochnel  41721  dihjat1  41757  dvh4dimlem  41771  dochsnkr2cl  41802  dochkr1  41806  dochkr1OLDN  41807  lcfl6lem  41826  lcfl9a  41833  lclkrlem2l  41846  lclkrlem2o  41849  lclkrlem2q  41851  lcfrlem9  41878  lcfrlem16  41886  lcfrlem17  41887  lcfrlem27  41897  lcfrlem37  41907  lcfrlem38  41908  lcfrlem40  41910  lcdlkreqN  41950  mapdrvallem2  41973  mapdn0  41997  mapdpglem20  42019  mapdpglem30  42030  mapdindp0  42047  mapdhcl  42055  mapdh6aN  42063  mapdh6dN  42067  mapdh6eN  42068  mapdh6kN  42074  mapdh8  42116  hdmap1l6a  42137  hdmap1l6d  42141  hdmap1l6e  42142  hdmap1l6k  42148  hdmapval3N  42166  hdmap10  42168  hdmap11lem2  42170  hdmapnzcl  42173  hdmaprnlem3eN  42186  hdmaprnlem17N  42191  hdmap14lem4a  42199  hdmap14lem7  42202  hdmap14lem14  42209  hgmaprnlem5N  42228  hdmaplkr  42241  hdmapip0  42243  hgmapvvlem2  42252  hgmapvvlem3  42253  hgmapvv  42254  redvmptabs  42682  readvrec2  42683  readvrec  42684  fiabv  42858  fsuppind  42900  0prjspnlem  42933  pellexlem5  43142  dfac11  43371  dfacbasgrp  43417  dgraalem  43454  dgraaub  43457  aaitgo  43471  proot1ex  43505  deg1mhm  43509  ofdivrec  44634  ofdivcan4  44635  ofdivdiv2  44636  expgrowth  44643  binomcxplemnotnn0  44664  dvdivbd  46234  dvdivcncf  46238  dirkeritg  46413  fourierdlem39  46457  fourierdlem57  46474  fourierdlem58  46475  fourierdlem59  46476  fourierdlem68  46485  fourierdlem76  46493  fourierdlem103  46520  fourierdlem104  46521  fourierdlem111  46528  setsnidel  47690  sprvalpwn0  47796  odz2prm2pw  47876  fmtnoprmfac1  47878  fmtnoprmfac2  47880  sfprmdvdsmersenne  47916  lighneallem2  47919  lighneallem3  47920  lighneal  47924  oddprmALTV  48000  evenprm2  48027  oddprmne2  48028  odd2prm2  48031  even3prm2  48032  isubgruhgr  48181  grimuhgr  48200  2zrngnmrid  48569  lincext1  48767  lindslinindsimp2lem5  48775  rege1logbrege0  48871  fllogbd  48873  relogbmulbexp  48874  relogbdivb  48875  nnpw2blen  48893  blennngt2o2  48905  blennn0e2  48907  dignn0ldlem  48915  line  49045  rrxline  49047  aacllem  50113