Theorem eldifsn 4811

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   ≠ wne 2946   ∖ cdif 3973  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-sn 4649

This theorem is referenced by:  eldifsnd  4812  elpwdifsn  4814  eldifsni  4815  rexdifsn  4819  raldifsni  4820  eldifvsn  4822  difsn  4823  sossfld  6217  tpres  7238  onmindif2  7843  xpord3pred  8193  xpord3inddlem  8195  mptsuppd  8228  suppssr  8236  suppssov1  8238  suppssov2  8239  suppsssn  8242  suppssfv  8243  dif1o  8556  difsnen  9119  limenpsi  9218  frfi  9349  fofinf1o  9400  en2eleq  10077  en2other2  10078  dfac8clem  10101  acni2  10115  acndom  10120  acnnum  10121  dfac9  10206  dfacacn  10211  kmlem3  10222  kmlem4  10223  fin23lem21  10408  canthp1lem2  10722  elni  10945  mulnzcnf  11936  divval  11951  elnnne0  12567  elq  13015  rpcndif0  13076  modfzo0difsn  13994  modsumfzodifsn  13995  expcl2lem  14124  expclzlem  14134  hashdifpr  14464  hashgt23el  14473  prprrab  14522  hashle2prv  14527  reccn2  15643  rlimdiv  15694  eff2  16147  tanval  16176  rpnnen2lem9  16270  fzo0dvdseq  16371  oddprmgt2  16746  oddprmdvds  16950  4sqlem19  17010  prmlem0  17153  prmlem1a  17154  setsnid  17256  setsnidOLD  17257  grpinvnzcl  19051  symgextf  19459  f1omvdmvd  19485  pmtrprfv  19495  odcau  19646  efgsf  19771  efgsrel  19776  efgs1  19777  efgs1b  19778  efgsp1  19779  efgsres  19780  efgredlema  19782  efgredlemd  19786  efgrelexlemb  19792  gsumpt  20004  dmdprdd  20043  dprdcntz  20052  dprdfeq0  20066  dprd2da  20086  isdomn2OLD  20734  domnrrg  20735  isdomn3  20737  drngunit  20756  isdrng2  20765  drngmcl  20772  drngid2  20774  isdrngd  20787  isdrngdOLD  20789  issubdrg  20803  sdrgacs  20824  cntzsdrg  20825  islss  20955  lssneln0  20974  lssssr  20975  lbsind  21102  lbspss  21104  lspabs3  21146  lspsneq  21147  lspfixed  21153  lspexch  21154  islbs2  21179  cnflddivOLD  21437  cnfldinv  21438  xrs1mnd  21445  xrs10  21446  xrge0subm  21448  cnsubdrglem  21459  cnmgpid  21470  cnmsubglem  21471  gzrngunit  21474  zringunit  21500  zringndrg  21502  domnchr  21570  cnmsgngrp  21620  psgninv  21623  psgndiflemB  21641  lindfind  21859  lindsind  21860  lindff1  21863  lindfrn  21864  mvrcl  22035  coe1tmmul2  22300  mdetunilem9  22647  maducoeval2  22667  gsummatr01lem4  22685  ist1-2  23376  cmpfi  23437  2ndcdisj  23485  2ndcsep  23488  locfincmp  23555  alexsublem  24073  cldsubg  24140  imasdsf1olem  24404  prdsxmslem2  24563  reperflem  24859  xrge0gsumle  24874  xrge0tsms  24875  divcnOLD  24909  divcn  24911  evth  25010  cvsdiv  25184  cvsdivcl  25185  cphreccllem  25231  bcthlem5  25381  itg11  25745  i1fmullem  25748  i1fadd  25749  itg1addlem2  25751  i1fmulc  25758  itg1mulc  25759  ellimc3  25934  limcmpt2  25939  dvlem  25951  dvidlem  25970  dvcnp  25974  dvcobr  26003  dvcobrOLD  26004  dvrec  26013  dvrecg  26031  dvmptdiv  26032  dvcnvlem  26034  dvexp3  26036  dveflem  26037  dvferm1lem  26042  dvferm2lem  26044  lhop1lem  26072  ftc1lem5  26101  mdegleb  26123  coe1mul3  26158  ply1nz  26181  fta1blem  26230  fta1b  26231  ig1peu  26234  ig1pdvds  26239  plyeq0lem  26269  dgrub  26293  quotval  26352  fta1lem  26367  fta1  26368  elqaalem3  26381  qaa  26383  iaa  26385  aareccl  26386  aannenlem2  26389  abelthlem8  26501  abelth  26503  eff1olem  26608  logrncl  26627  eflog  26636  logeftb  26643  logdmss  26702  dvlog  26711  logbcl  26828  logbid1  26829  logb1  26830  elogb  26831  logbchbase  26832  relogbval  26833  relogbcl  26834  relogbreexp  26836  relogbmul  26838  nnlogbexp  26842  relogbcxp  26846  cxplogb  26847  relogbcxpb  26848  logbf  26850  logblog  26853  2logb9irrALT  26859  sqrt2cxp2logb9e3  26860  angval  26862  dcubic  26907  rlimcnp  27026  efrlim  27030  efrlimOLD  27031  logexprlim  27287  dchrghm  27318  dchrabs  27322  lgsfcl2  27365  lgsval2lem  27369  lgsval3  27377  lgsmod  27385  lgsdirprm  27393  lgsne0  27397  gausslemma2dlem0f  27423  lgsquad2lem2  27447  2lgsoddprm  27478  2sqlem11  27491  2sqblem  27493  dchrvmaeq0  27566  rpvmasum2  27574  dchrisum0re  27575  qrngdiv  27686  addsval  28013  divsval  28233  elnns  28361  1nns  28370  tglngval  28577  tgisline  28653  axlowdimlem9  28983  axlowdimlem12  28986  axlowdimlem13  28987  elntg2  29018  upgrbi  29128  upgr1elem  29147  umgrislfupgrlem  29157  edgupgr  29169  subgruhgredgd  29319  upgrreslem  29339  nbgrel  29375  nbupgr  29379  nbupgrel  29380  nbumgrvtx  29381  nbgrssovtx  29396  nbupgrres  29399  nbusgrvtxm1uvtx  29440  nbupgruvtxres  29442  iscplgredg  29452  cusgredg  29459  cusgrfilem2  29492  usgredgsscusgredg  29495  1loopgrnb0  29538  1egrvtxdg0  29547  uhgrvd00  29570  vtxdginducedm1lem4  29578  eupth2lem3lem3  30262  frcond1  30298  frcond4  30302  2pthfrgr  30316  3cyclfrgrrn1  30317  n4cyclfrgr  30323  frgrwopreglem4a  30342  numclwwlk5  30420  ressupprn  32702  suppss3  32738  xdivval  32883  xrge0tsmsd  33041  pmtrcnel  33082  pmtrcnelor  33084  0nellinds  33363  dvdsruasso  33378  mxidlirredi  33464  extdg1id  33676  irngnzply1  33691  submatminr1  33756  ordtconnlem1  33870  ispisys2  34117  sigapisys  34119  sibfinima  34304  sseqf  34357  signswch  34538  signstfvn  34546  signsvtn0  34547  signstfvneq0  34549  signstfvcl  34550  signstfveq0a  34553  signstfveq0  34554  signsvfn  34559  signsvtp  34560  signsvtn  34561  signsvfpn  34562  signsvfnn  34563  signlem0  34564  bnj158  34705  bnj168  34706  bnj529  34717  bnj906  34906  bnj970  34923  exdifsn  35055  cusgredgex2  35090  subfacp1lem5  35152  cvmsi  35233  cvmsval  35234  cvmsdisj  35238  cvmscld  35241  cvmsss2  35242  satfv1lem  35330  sinccvglem  35640  circum  35642  mpomulnzcnf  36265  unbdqndv2lem2  36476  bj-0int  37067  lindsadd  37573  lindsenlbs  37575  matunitlindflem2  37577  matunitlindf  37578  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem16  37596  poimirlem18  37598  poimirlem19  37599  poimirlem21  37601  poimirlem22  37602  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  itg2addnclem2  37632  sdclem1  37703  rrncmslem  37792  rrnequiv  37795  isdrngo2  37918  isdrngo3  37919  prtlem100  38815  prter2  38837  prter3  38838  lsatlspsn2  38948  lsateln0  38951  lsatn0  38955  lsatspn0  38956  lsatcmp  38959  lsatelbN  38962  islshpat  38973  lsat0cv  38989  lkrlspeqN  39127  dvheveccl  41069  dihlatat  41294  dochnel  41350  dihjat1  41386  dvh4dimlem  41400  dochsnkr2cl  41431  dochkr1  41435  dochkr1OLDN  41436  lcfl6lem  41455  lcfl9a  41462  lclkrlem2l  41475  lclkrlem2o  41478  lclkrlem2q  41480  lcfrlem9  41507  lcfrlem16  41515  lcfrlem17  41516  lcfrlem27  41526  lcfrlem37  41536  lcfrlem38  41537  lcfrlem40  41539  lcdlkreqN  41579  mapdrvallem2  41602  mapdn0  41626  mapdpglem20  41648  mapdpglem30  41659  mapdindp0  41676  mapdhcl  41684  mapdh6aN  41692  mapdh6dN  41696  mapdh6eN  41697  mapdh6kN  41703  mapdh8  41745  hdmap1l6a  41766  hdmap1l6d  41770  hdmap1l6e  41771  hdmap1l6k  41777  hdmapval3N  41795  hdmap10  41797  hdmap11lem2  41799  hdmapnzcl  41802  hdmaprnlem3eN  41815  hdmaprnlem17N  41820  hdmap14lem4a  41828  hdmap14lem7  41831  hdmap14lem14  41838  hgmaprnlem5N  41857  hdmaplkr  41870  hdmapip0  41872  hgmapvvlem2  41881  hgmapvvlem3  41882  hgmapvv  41883  fiabv  42491  fsuppind  42545  0prjspnlem  42578  pellexlem5  42789  dfac11  43019  dfacbasgrp  43065  dgraalem  43102  dgraaub  43105  aaitgo  43119  proot1ex  43157  deg1mhm  43161  ofdivrec  44295  ofdivcan4  44296  ofdivdiv2  44297  expgrowth  44304  binomcxplemnotnn0  44325  dvdivbd  45844  dvdivcncf  45848  dirkeritg  46023  fourierdlem39  46067  fourierdlem57  46084  fourierdlem58  46085  fourierdlem59  46086  fourierdlem68  46095  fourierdlem76  46103  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  setsnidel  47251  sprvalpwn0  47357  odz2prm2pw  47437  fmtnoprmfac1  47439  fmtnoprmfac2  47441  sfprmdvdsmersenne  47477  lighneallem2  47480  lighneallem3  47481  lighneal  47485  oddprmALTV  47561  evenprm2  47588  oddprmne2  47589  odd2prm2  47592  even3prm2  47593  isubgruhgr  47738  grimuhgr  47762  2zrngnmrid  47979  lincext1  48183  lindslinindsimp2lem5  48191  rege1logbrege0  48292  fllogbd  48294  relogbmulbexp  48295  relogbdivb  48296  nnpw2blen  48314  blennngt2o2  48326  blennn0e2  48328  dignn0ldlem  48336  line  48466  rrxline  48468  aacllem  48895