Theorem eldifsn 4748

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 4052	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4598	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2996	. . 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 2147   ≠ wne 2959   ∖ cdif 4048  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-dif 4050  df-sn 4589

This theorem is used by:  eldifsnbd  4749  eldifsnd  4750  eldifsni  4753  rexdifsn  4757  raldifsni  4758  eldifvsn  4760  difsn  4761  sossfld  6189  tpres  7227  onmindif2  7842  xpord3pred  8193  xpord3inddlem  8195  mptsuppd  8229  suppssr  8237  suppssov1  8239  suppssov2  8240  suppsssn  8243  suppssfv  8244  dif1o  8533  difsnen  9103  limenpsi  9196  frfi  9301  fofinf1o  9346  en2eleq  10111  en2other2  10112  dfac8clem  10135  acni2  10149  acndom  10154  acnnum  10155  dfac9  10239  dfacacn  10244  kmlem3  10255  kmlem4  10256  fin23lem21  10441  canthp1lem2  10762  elni  10985  mulnzcnf  11986  divval  12000  elnnne0  12644  elq  13101  rpcndif0  13165  modfzo0difsn  14110  modsumfzodifsn  14111  expcl2lem  14240  expclzlem  14250  hashdifpr  14584  hashgt23el  14593  prprrab  14642  hashle2prv  14647  reccn2  15790  rlimdiv  15839  eff2  16293  tanval  16322  rpnnen2lem9  16416  fzo0dvdseq  16519  oddprmgt2  16901  oddprmdvds  17107  4sqlem19  17167  prmlem0  17309  prmlem1a  17310  setsnid  17412  grpinvnzcl  19247  symgextf  19658  f1omvdmvd  19684  pmtrprfv  19694  odcau  19845  efgsf  19970  efgsrel  19975  efgs1  19976  efgs1b  19977  efgsp1  19978  efgsres  19979  efgredlema  19981  efgredlemd  19985  efgrelexlemb  19991  gsumpt  20203  dmdprdd  20242  dprdcntz  20251  dprdfeq0  20265  dprd2da  20285  domnrrg  20991  isdomn3  20993  drngunit  21012  isdrng3lem2  21033  isdrng5  21035  drngmcl  21036  drngid2  21037  isdrngd  21049  isdrngdOLD  21051  issubdrg  21064  sdrgacs  21085  cntzsdrg  21086  islss  21236  lssneln0  21255  lssssr  21256  lbsind  21382  lbspss  21384  lspabs3  21426  lspsneq  21427  lspfixed  21433  lspexch  21434  islbs2  21459  cnfldinv  21736  cnsubdrglem  21751  cnmgpid  21762  cnmsubglem  21763  gzrngunit  21766  xrs1mnd  21773  xrs10  21774  xrge0subm  21776  zringunit  21799  zringndrg  21801  domnchr  21865  cnmsgngrp  21912  psgninv  21915  psgndiflemB  21933  lindfind  22149  lindsind  22150  lindff1  22153  lindfrn  22154  lindsenlbs  22184  mvrcl  22326  coe1tmmul2  22622  mdetunilem9  22962  maducoeval2  22982  gsummatr01lem4  23000  matunitlindflem2  23022  matunitlindf  23023  ist1-2  23692  cmpfi  23753  2ndcdisj  23802  2ndcsep  23805  locfincmp  23872  alexsublem  24390  cldsubg  24457  imasdsf1olem  24719  prdsxmslem2  24875  reperflem  25165  xrge0gsumle  25180  xrge0tsms  25181  divcn  25216  evth  25307  cvsdiv  25480  cvsdivcl  25481  cphreccllem  25526  bcthlem5  25676  itg11  26039  i1fmullem  26042  i1fadd  26043  itg1addlem2  26045  i1fmulc  26051  itg1mulc  26052  ellimc3  26226  limcmpt2  26231  dvlem  26243  dvidlem  26262  dvcnp  26266  dvcobr  26293  dvrec  26302  dvrecg  26320  dvmptdiv  26321  dvcnvlem  26323  dvexp3  26325  dveflem  26326  dvferm1lem  26331  dvferm2lem  26333  lhop1lem  26360  ftc1lem5  26387  mdegleb  26409  coe1mul3  26444  ply1nz  26467  fta1blem  26516  fta1b  26517  ig1peu  26520  ig1pdvds  26525  plyeq0lem  26556  dgrub  26580  quotval  26640  fta1lem  26655  fta1  26656  elqaalem3  26671  iaaOLD  26679  aareccl  26680  aannenlem2  26683  abelthlem8  26793  abelth  26795  eff1olem  26903  logrncl  26922  eflog  26931  logeftb  26938  logdmss  26997  dvlog  27006  logbcl  27122  logbid1  27123  logb1  27124  elogb  27125  logbchbase  27126  relogbval  27127  relogbcl  27128  relogbreexp  27130  relogbmul  27132  nnlogbexp  27136  relogbcxp  27140  cxplogb  27141  relogbcxpb  27142  logbf  27144  logblog  27147  2logb9irrALT  27153  sqrt2cxp2logb9e3  27154  angval  27156  dcubic  27201  rlimcnp  27320  efrlim  27324  logexprlim  27579  dchrghm  27610  dchrabs  27614  lgsfcl2  27657  lgsval2lem  27661  lgsval3  27669  lgsmod  27677  lgsdirprm  27685  lgsne0  27689  gausslemma2dlem0f  27715  lgsquad2lem2  27739  2lgsoddprm  27770  2sqlem11  27783  2sqblem  27785  dchrvmaeq0  27858  rpvmasum2  27866  dchrisum0re  27867  qrngdiv  27978  fltoprmlem1  28020  addsval  28375  divsval  28602  elnns  28753  1nns  28762  tglngval  29041  tgisline  29122  axlowdimlem9  29555  axlowdimlem12  29558  axlowdimlem13  29559  elntg2  29590  upgrbi  29698  upgr1elem  29717  umgrislfupgrlem  29727  edgupgr  29739  subgruhgredgd  29892  upgrreslem  29912  nbgrel  29948  nbupgr  29952  nbupgrel  29953  nbumgrvtx  29954  nbgrssovtx  29969  nbupgrres  29972  nbusgrvtxm1uvtx  30013  nbupgruvtxres  30015  iscplgredg  30025  cusgredg  30032  cusgrfilem2  30064  usgredgsscusgredg  30067  1loopgrnb0  30110  1egrvtxdg0  30119  uhgrvd00  30142  vtxdginducedm1lem4  30150  eupth2lem3lem3  30858  frcond1  30894  frcond4  30898  2pthfrgr  30912  3cyclfrgrrn1  30913  n4cyclfrgr  30919  frgrwopreglem4a  30938  numclwwlk5  31016  ressupprn  33351  suppss3  33382  xdivval  33552  xrge0tsmsd  33701  pmtrcnel  33717  pmtrcnelor  33719  0nellinds  33993  dvdsruasso  34007  extdg1id  34365  irngnzply1  34390  submatminr1  34509  ordtconnlem1  34623  ispisys2  34853  sigapisys  34855  sibfinima  35038  sseqf  35091  signswch  35257  signstfvn  35265  signsvtn0  35266  signstfvneq0  35268  signstfvcl  35269  signstfveq0a  35272  signstfveq0  35273  signsvfn  35278  signsvtp  35279  signsvtn  35280  signsvfpn  35281  signsvfnn  35282  signlem0  35283  bnj158  35427  bnj168  35428  bnj529  35439  bnj906  35627  bnj970  35644  exdifsn  35780  suceldifsn0  35788  soinfdom  35797  cusgredgex2  36063  subfacp1lem5  36115  cvmsi  36196  cvmsval  36197  cvmsdisj  36201  cvmscld  36204  cvmsss2  36205  satfv1lem  36293  sinccvglem  36603  circum  36605  mpomulnzcnf  37265  unbdqndv2lem2  37553  bj-0int  38212  lindsadd  38727  poimirlem6  38735  poimirlem7  38736  poimirlem8  38737  poimirlem16  38745  poimirlem18  38747  poimirlem19  38748  poimirlem21  38750  poimirlem22  38751  poimirlem24  38753  poimirlem25  38754  poimirlem26  38755  poimirlem27  38756  itg2addnclem2  38781  sdclem1  38868  rrncmslem  38957  rrnequiv  38960  isdrngo2  39083  isdrngo3  39084  eldmxrncnvepres  39557  eldmxrncnvepres2  39558  prtlem100  40107  prter2  40129  prter3  40130  lsatlspsn2  40240  lsateln0  40243  lsatn0  40247  lsatspn0  40248  lsatcmp  40251  lsatelbN  40254  islshpat  40265  lsat0cv  40281  lkrlspeqN  40419  dvheveccl  42360  dihlatat  42585  dochnel  42641  dihjat1  42677  dvh4dimlem  42691  dochsnkr2cl  42722  dochkr1  42726  dochkr1OLDN  42727  lcfl6lem  42746  lcfl9a  42753  lclkrlem2l  42766  lclkrlem2o  42769  lclkrlem2q  42771  lcfrlem9  42798  lcfrlem16  42806  lcfrlem17  42807  lcfrlem27  42817  lcfrlem37  42827  lcfrlem38  42828  lcfrlem40  42830  lcdlkreqN  42870  mapdrvallem2  42893  mapdn0  42917  mapdpglem20  42939  mapdpglem30  42950  mapdindp0  42967  mapdhcl  42975  mapdh6aN  42983  mapdh6dN  42987  mapdh6eN  42988  mapdh6kN  42994  mapdh8  43036  hdmap1l6a  43057  hdmap1l6d  43061  hdmap1l6e  43062  hdmap1l6k  43068  hdmapval3N  43086  hdmap10  43088  hdmap11lem2  43090  hdmapnzcl  43093  hdmaprnlem3eN  43106  hdmaprnlem17N  43111  hdmap14lem4a  43119  hdmap14lem7  43122  hdmap14lem14  43129  hgmaprnlem5N  43148  hdmaplkr  43161  hdmapip0  43163  hgmapvvlem2  43172  hgmapvvlem3  43173  hgmapvv  43174  redvmptabs  43602  readvrec2  43603  readvrec  43604  fiabv  43791  fsuppind  43809  prjspnnorm  43852  0prjspnlem  43853  pellexlem5  44031  dfac11  44255  dfacbasgrp  44300  dgraalem  44337  dgraaub  44340  aaitgo  44354  proot1ex  44388  deg1mhm  44392  ofdivrec  45500  ofdivcan4  45501  ofdivdiv2  45502  expgrowth  45509  binomcxplemnotnn0  45530  dvdivbd  47136  dvdivcncf  47140  dirkeritg  47315  fourierdlem39  47359  fourierdlem57  47376  fourierdlem58  47377  fourierdlem59  47378  fourierdlem68  47387  fourierdlem76  47395  fourierdlem103  47422  fourierdlem104  47423  fourierdlem111  47430  setsnidel  48662  sprvalpwn0  48768  odz2prm2pw  48851  fmtnoprmfac1  48853  fmtnoprmfac2  48855  sfprmdvdsmersenne  48891  lighneallem2  48894  lighneallem3  48895  lighneal  48899  oddprmALTV  48988  evenprm2  49015  oddprmne2  49016  odd2prm2  49019  even3prm2  49020  isubgruhgr  49169  grimuhgr  49188  2zrngnmrid  49556  lincext1  49769  lindslinindsimp2lem5  49777  rege1logbrege0  49873  fllogbd  49875  relogbmulbexp  49876  relogbdivb  49877  nnpw2blen  49895  blennngt2o2  49907  blennn0e2  49909  dignn0ldlem  49917  line  50048  rrxline  50050  dvsec  51134  dvcsc  51135  dvcot  51136  aacllem  51217  veroquadmodzerod  51262  veroquadnolindfd  51263