Theorem eldifsn 4747

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 4049	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4597	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2992	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 585	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 278	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∈ wcel 2144   ≠ wne 2955   ∖ cdif 4045  {csn 4583

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 4047  df-sn 4584

This theorem is used by:  eldifsnbd  4748  eldifsnd  4749  eldifsni  4752  rexdifsn  4756  raldifsni  4757  eldifvsn  4759  difsn  4760  sossfld  6177  tpres  7207  onmindif2  7821  xpord3pred  8169  xpord3inddlem  8171  mptsuppd  8204  suppssr  8212  suppssov1  8214  suppssov2  8215  suppsssn  8218  suppssfv  8219  dif1o  8508  difsnen  9078  limenpsi  9171  frfi  9276  fofinf1o  9321  en2eleq  10087  en2other2  10088  dfac8clem  10111  acni2  10125  acndom  10130  acnnum  10131  dfac9  10215  dfacacn  10220  kmlem3  10231  kmlem4  10232  fin23lem21  10417  canthp1lem2  10738  elni  10961  mulnzcnf  11962  divval  11976  elnnne0  12620  elq  13077  rpcndif0  13141  modfzo0difsn  14086  modsumfzodifsn  14087  expcl2lem  14216  expclzlem  14226  hashdifpr  14560  hashgt23el  14569  prprrab  14618  hashle2prv  14623  reccn2  15764  rlimdiv  15813  eff2  16267  tanval  16296  rpnnen2lem9  16390  fzo0dvdseq  16493  oddprmgt2  16875  oddprmdvds  17081  4sqlem19  17141  prmlem0  17283  prmlem1a  17284  setsnid  17386  grpinvnzcl  19221  symgextf  19631  f1omvdmvd  19657  pmtrprfv  19667  odcau  19818  efgsf  19943  efgsrel  19948  efgs1  19949  efgs1b  19950  efgsp1  19951  efgsres  19952  efgredlema  19954  efgredlemd  19958  efgrelexlemb  19964  gsumpt  20176  dmdprdd  20215  dprdcntz  20224  dprdfeq0  20238  dprd2da  20258  domnrrg  20964  isdomn3  20966  drngunit  20985  isdrng3lem2  21006  isdrng5  21008  drngmcl  21009  drngid2  21010  isdrngd  21022  isdrngdOLD  21024  issubdrg  21037  sdrgacs  21058  cntzsdrg  21059  islss  21209  lssneln0  21228  lssssr  21229  lbsind  21355  lbspss  21357  lspabs3  21399  lspsneq  21400  lspfixed  21406  lspexch  21407  islbs2  21432  cnfldinv  21709  cnsubdrglem  21724  cnmgpid  21735  cnmsubglem  21736  gzrngunit  21739  xrs1mnd  21746  xrs10  21747  xrge0subm  21749  zringunit  21772  zringndrg  21774  domnchr  21838  cnmsgngrp  21885  psgninv  21888  psgndiflemB  21906  lindfind  22122  lindsind  22123  lindff1  22126  lindfrn  22127  lindsenlbs  22157  mvrcl  22299  coe1tmmul2  22595  mdetunilem9  22935  maducoeval2  22955  gsummatr01lem4  22973  matunitlindflem2  22995  matunitlindf  22996  ist1-2  23665  cmpfi  23726  2ndcdisj  23775  2ndcsep  23778  locfincmp  23845  alexsublem  24363  cldsubg  24430  imasdsf1olem  24692  prdsxmslem2  24848  reperflem  25138  xrge0gsumle  25153  xrge0tsms  25154  divcn  25189  evth  25280  cvsdiv  25453  cvsdivcl  25454  cphreccllem  25499  bcthlem5  25649  itg11  26012  i1fmullem  26015  i1fadd  26016  itg1addlem2  26018  i1fmulc  26024  itg1mulc  26025  ellimc3  26199  limcmpt2  26204  dvlem  26216  dvidlem  26235  dvcnp  26239  dvcobr  26266  dvrec  26275  dvrecg  26293  dvmptdiv  26294  dvcnvlem  26296  dvexp3  26298  dveflem  26299  dvferm1lem  26304  dvferm2lem  26306  lhop1lem  26333  ftc1lem5  26360  mdegleb  26382  coe1mul3  26417  ply1nz  26440  fta1blem  26489  fta1b  26490  ig1peu  26493  ig1pdvds  26498  plyeq0lem  26529  dgrub  26553  quotval  26613  fta1lem  26628  fta1  26629  elqaalem3  26644  qaa  26647  iaaOLD  26652  aareccl  26653  aannenlem2  26656  abelthlem8  26766  abelth  26768  eff1olem  26876  logrncl  26895  eflog  26904  logeftb  26911  logdmss  26970  dvlog  26979  logbcl  27095  logbid1  27096  logb1  27097  elogb  27098  logbchbase  27099  relogbval  27100  relogbcl  27101  relogbreexp  27103  relogbmul  27105  nnlogbexp  27109  relogbcxp  27113  cxplogb  27114  relogbcxpb  27115  logbf  27117  logblog  27120  2logb9irrALT  27126  sqrt2cxp2logb9e3  27127  angval  27129  dcubic  27174  rlimcnp  27293  efrlim  27297  logexprlim  27552  dchrghm  27583  dchrabs  27587  lgsfcl2  27630  lgsval2lem  27634  lgsval3  27642  lgsmod  27650  lgsdirprm  27658  lgsne0  27662  gausslemma2dlem0f  27688  lgsquad2lem2  27712  2lgsoddprm  27743  2sqlem11  27756  2sqblem  27758  dchrvmaeq0  27831  rpvmasum2  27839  dchrisum0re  27840  qrngdiv  27951  fltoprmlem1  27993  addsval  28348  divsval  28575  elnns  28726  1nns  28735  tglngval  29014  tgisline  29095  axlowdimlem9  29528  axlowdimlem12  29531  axlowdimlem13  29532  elntg2  29563  upgrbi  29671  upgr1elem  29690  umgrislfupgrlem  29700  edgupgr  29712  subgruhgredgd  29865  upgrreslem  29885  nbgrel  29921  nbupgr  29925  nbupgrel  29926  nbumgrvtx  29927  nbgrssovtx  29942  nbupgrres  29945  nbusgrvtxm1uvtx  29986  nbupgruvtxres  29988  iscplgredg  29998  cusgredg  30005  cusgrfilem2  30037  usgredgsscusgredg  30040  1loopgrnb0  30083  1egrvtxdg0  30092  uhgrvd00  30115  vtxdginducedm1lem4  30123  eupth2lem3lem3  30831  frcond1  30867  frcond4  30871  2pthfrgr  30885  3cyclfrgrrn1  30886  n4cyclfrgr  30892  frgrwopreglem4a  30911  numclwwlk5  30989  ressupprn  33325  suppss3  33357  xdivval  33527  xrge0tsmsd  33676  pmtrcnel  33692  pmtrcnelor  33694  0nellinds  33968  dvdsruasso  33982  extdg1id  34340  irngnzply1  34365  submatminr1  34484  ordtconnlem1  34598  ispisys2  34828  sigapisys  34830  sibfinima  35013  sseqf  35066  signswch  35232  signstfvn  35240  signsvtn0  35241  signstfvneq0  35243  signstfvcl  35244  signstfveq0a  35247  signstfveq0  35248  signsvfn  35253  signsvtp  35254  signsvtn  35255  signsvfpn  35256  signsvfnn  35257  signlem0  35258  bnj158  35402  bnj168  35403  bnj529  35414  bnj906  35602  bnj970  35619  exdifsn  35753  soinfdom  35759  cusgredgex2  35949  subfacp1lem5  35991  cvmsi  36072  cvmsval  36073  cvmsdisj  36077  cvmscld  36080  cvmsss2  36081  satfv1lem  36169  sinccvglem  36479  circum  36481  mpomulnzcnf  37130  unbdqndv2lem2  37418  bj-0int  38064  lindsadd  38579  poimirlem6  38587  poimirlem7  38588  poimirlem8  38589  poimirlem16  38597  poimirlem18  38599  poimirlem19  38600  poimirlem21  38602  poimirlem22  38603  poimirlem24  38605  poimirlem25  38606  poimirlem26  38607  poimirlem27  38608  itg2addnclem2  38633  sdclem1  38720  rrncmslem  38809  rrnequiv  38812  isdrngo2  38935  isdrngo3  38936  eldmxrncnvepres  39409  eldmxrncnvepres2  39410  prtlem100  39959  prter2  39981  prter3  39982  lsatlspsn2  40092  lsateln0  40095  lsatn0  40099  lsatspn0  40100  lsatcmp  40103  lsatelbN  40106  islshpat  40117  lsat0cv  40133  lkrlspeqN  40271  dvheveccl  42212  dihlatat  42437  dochnel  42493  dihjat1  42529  dvh4dimlem  42543  dochsnkr2cl  42574  dochkr1  42578  dochkr1OLDN  42579  lcfl6lem  42598  lcfl9a  42605  lclkrlem2l  42618  lclkrlem2o  42621  lclkrlem2q  42623  lcfrlem9  42650  lcfrlem16  42658  lcfrlem17  42659  lcfrlem27  42669  lcfrlem37  42679  lcfrlem38  42680  lcfrlem40  42682  lcdlkreqN  42722  mapdrvallem2  42745  mapdn0  42769  mapdpglem20  42791  mapdpglem30  42802  mapdindp0  42819  mapdhcl  42827  mapdh6aN  42835  mapdh6dN  42839  mapdh6eN  42840  mapdh6kN  42846  mapdh8  42888  hdmap1l6a  42909  hdmap1l6d  42913  hdmap1l6e  42914  hdmap1l6k  42920  hdmapval3N  42938  hdmap10  42940  hdmap11lem2  42942  hdmapnzcl  42945  hdmaprnlem3eN  42958  hdmaprnlem17N  42963  hdmap14lem4a  42971  hdmap14lem7  42974  hdmap14lem14  42981  hgmaprnlem5N  43000  hdmaplkr  43013  hdmapip0  43015  hgmapvvlem2  43024  hgmapvvlem3  43025  hgmapvv  43026  redvmptabs  43454  readvrec2  43455  readvrec  43456  fiabv  43643  fsuppind  43661  prjspnnorm  43704  0prjspnlem  43705  pellexlem5  43882  dfac11  44106  dfacbasgrp  44152  dgraalem  44189  dgraaub  44192  aaitgo  44206  proot1ex  44240  deg1mhm  44244  ofdivrec  45352  ofdivcan4  45353  ofdivdiv2  45354  expgrowth  45361  binomcxplemnotnn0  45382  dvdivbd  46975  dvdivcncf  46979  dirkeritg  47154  fourierdlem39  47198  fourierdlem57  47215  fourierdlem58  47216  fourierdlem59  47217  fourierdlem68  47226  fourierdlem76  47234  fourierdlem103  47261  fourierdlem104  47262  fourierdlem111  47269  setsnidel  48501  sprvalpwn0  48607  odz2prm2pw  48690  fmtnoprmfac1  48692  fmtnoprmfac2  48694  sfprmdvdsmersenne  48730  lighneallem2  48733  lighneallem3  48734  lighneal  48738  oddprmALTV  48827  evenprm2  48854  oddprmne2  48855  odd2prm2  48858  even3prm2  48859  isubgruhgr  49008  grimuhgr  49027  2zrngnmrid  49395  lincext1  49608  lindslinindsimp2lem5  49616  rege1logbrege0  49712  fllogbd  49714  relogbmulbexp  49715  relogbdivb  49716  nnpw2blen  49734  blennngt2o2  49746  blennn0e2  49748  dignn0ldlem  49756  line  49886  rrxline  49888  dvsec  50898  dvcsc  50899  dvcot  50900  aacllem  50981  veroquadmodzerod  51026  veroquadnolindfd  51027