Theorem eldifsn 4753

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   ≠ wne 2926   ∖ cdif 3914  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-sn 4593

This theorem is referenced by:  eldifsnd  4754  elpwdifsn  4756  eldifsni  4757  rexdifsn  4761  raldifsni  4762  eldifvsn  4764  difsn  4765  sossfld  6162  tpres  7178  onmindif2  7786  xpord3pred  8134  xpord3inddlem  8136  mptsuppd  8169  suppssr  8177  suppssov1  8179  suppssov2  8180  suppsssn  8183  suppssfv  8184  dif1o  8467  difsnen  9027  limenpsi  9122  frfi  9239  fofinf1o  9290  en2eleq  9968  en2other2  9969  dfac8clem  9992  acni2  10006  acndom  10011  acnnum  10012  dfac9  10097  dfacacn  10102  kmlem3  10113  kmlem4  10114  fin23lem21  10299  canthp1lem2  10613  elni  10836  mulnzcnf  11831  divval  11846  elnnne0  12463  elq  12916  rpcndif0  12979  modfzo0difsn  13915  modsumfzodifsn  13916  expcl2lem  14045  expclzlem  14055  hashdifpr  14387  hashgt23el  14396  prprrab  14445  hashle2prv  14450  reccn2  15570  rlimdiv  15619  eff2  16074  tanval  16103  rpnnen2lem9  16197  fzo0dvdseq  16300  oddprmgt2  16676  oddprmdvds  16881  4sqlem19  16941  prmlem0  17083  prmlem1a  17084  setsnid  17185  grpinvnzcl  18950  symgextf  19354  f1omvdmvd  19380  pmtrprfv  19390  odcau  19541  efgsf  19666  efgsrel  19671  efgs1  19672  efgs1b  19673  efgsp1  19674  efgsres  19675  efgredlema  19677  efgredlemd  19681  efgrelexlemb  19687  gsumpt  19899  dmdprdd  19938  dprdcntz  19947  dprdfeq0  19961  dprd2da  19981  isdomn2OLD  20628  domnrrg  20629  isdomn3  20631  drngunit  20650  isdrng2  20659  drngmcl  20666  drngid2  20668  isdrngd  20681  isdrngdOLD  20683  issubdrg  20696  sdrgacs  20717  cntzsdrg  20718  islss  20847  lssneln0  20866  lssssr  20867  lbsind  20994  lbspss  20996  lspabs3  21038  lspsneq  21039  lspfixed  21045  lspexch  21046  islbs2  21071  cnflddivOLD  21320  cnfldinv  21321  xrs1mnd  21328  xrs10  21329  xrge0subm  21331  cnsubdrglem  21342  cnmgpid  21353  cnmsubglem  21354  gzrngunit  21357  zringunit  21383  zringndrg  21385  domnchr  21449  cnmsgngrp  21495  psgninv  21498  psgndiflemB  21516  lindfind  21732  lindsind  21733  lindff1  21736  lindfrn  21737  mvrcl  21908  coe1tmmul2  22169  mdetunilem9  22514  maducoeval2  22534  gsummatr01lem4  22552  ist1-2  23241  cmpfi  23302  2ndcdisj  23350  2ndcsep  23353  locfincmp  23420  alexsublem  23938  cldsubg  24005  imasdsf1olem  24268  prdsxmslem2  24424  reperflem  24714  xrge0gsumle  24729  xrge0tsms  24730  divcnOLD  24764  divcn  24766  evth  24865  cvsdiv  25039  cvsdivcl  25040  cphreccllem  25085  bcthlem5  25235  itg11  25599  i1fmullem  25602  i1fadd  25603  itg1addlem2  25605  i1fmulc  25611  itg1mulc  25612  ellimc3  25787  limcmpt2  25792  dvlem  25804  dvidlem  25823  dvcnp  25827  dvcobr  25856  dvcobrOLD  25857  dvrec  25866  dvrecg  25884  dvmptdiv  25885  dvcnvlem  25887  dvexp3  25889  dveflem  25890  dvferm1lem  25895  dvferm2lem  25897  lhop1lem  25925  ftc1lem5  25954  mdegleb  25976  coe1mul3  26011  ply1nz  26034  fta1blem  26083  fta1b  26084  ig1peu  26087  ig1pdvds  26092  plyeq0lem  26122  dgrub  26146  quotval  26207  fta1lem  26222  fta1  26223  elqaalem3  26236  qaa  26238  iaa  26240  aareccl  26241  aannenlem2  26244  abelthlem8  26356  abelth  26358  eff1olem  26464  logrncl  26483  eflog  26492  logeftb  26499  logdmss  26558  dvlog  26567  logbcl  26684  logbid1  26685  logb1  26686  elogb  26687  logbchbase  26688  relogbval  26689  relogbcl  26690  relogbreexp  26692  relogbmul  26694  nnlogbexp  26698  relogbcxp  26702  cxplogb  26703  relogbcxpb  26704  logbf  26706  logblog  26709  2logb9irrALT  26715  sqrt2cxp2logb9e3  26716  angval  26718  dcubic  26763  rlimcnp  26882  efrlim  26886  efrlimOLD  26887  logexprlim  27143  dchrghm  27174  dchrabs  27178  lgsfcl2  27221  lgsval2lem  27225  lgsval3  27233  lgsmod  27241  lgsdirprm  27249  lgsne0  27253  gausslemma2dlem0f  27279  lgsquad2lem2  27303  2lgsoddprm  27334  2sqlem11  27347  2sqblem  27349  dchrvmaeq0  27422  rpvmasum2  27430  dchrisum0re  27431  qrngdiv  27542  addsval  27876  divsval  28099  elnns  28239  1nns  28248  tglngval  28485  tgisline  28561  axlowdimlem9  28884  axlowdimlem12  28887  axlowdimlem13  28888  elntg2  28919  upgrbi  29027  upgr1elem  29046  umgrislfupgrlem  29056  edgupgr  29068  subgruhgredgd  29218  upgrreslem  29238  nbgrel  29274  nbupgr  29278  nbupgrel  29279  nbumgrvtx  29280  nbgrssovtx  29295  nbupgrres  29298  nbusgrvtxm1uvtx  29339  nbupgruvtxres  29341  iscplgredg  29351  cusgredg  29358  cusgrfilem2  29391  usgredgsscusgredg  29394  1loopgrnb0  29437  1egrvtxdg0  29446  uhgrvd00  29469  vtxdginducedm1lem4  29477  eupth2lem3lem3  30166  frcond1  30202  frcond4  30206  2pthfrgr  30220  3cyclfrgrrn1  30221  n4cyclfrgr  30227  frgrwopreglem4a  30246  numclwwlk5  30324  ressupprn  32620  suppss3  32654  xdivval  32846  xrge0tsmsd  33009  pmtrcnel  33053  pmtrcnelor  33055  0nellinds  33348  dvdsruasso  33363  mxidlirredi  33449  extdg1id  33668  irngnzply1  33693  submatminr1  33807  ordtconnlem1  33921  ispisys2  34150  sigapisys  34152  sibfinima  34337  sseqf  34390  signswch  34559  signstfvn  34567  signsvtn0  34568  signstfvneq0  34570  signstfvcl  34571  signstfveq0a  34574  signstfveq0  34575  signsvfn  34580  signsvtp  34581  signsvtn  34582  signsvfpn  34583  signsvfnn  34584  signlem0  34585  bnj158  34726  bnj168  34727  bnj529  34738  bnj906  34927  bnj970  34944  exdifsn  35076  cusgredgex2  35117  subfacp1lem5  35178  cvmsi  35259  cvmsval  35260  cvmsdisj  35264  cvmscld  35267  cvmsss2  35268  satfv1lem  35356  sinccvglem  35666  circum  35668  mpomulnzcnf  36294  unbdqndv2lem2  36505  bj-0int  37096  lindsadd  37614  lindsenlbs  37616  matunitlindflem2  37618  matunitlindf  37619  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem16  37637  poimirlem18  37639  poimirlem19  37640  poimirlem21  37642  poimirlem22  37643  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  itg2addnclem2  37673  sdclem1  37744  rrncmslem  37833  rrnequiv  37836  isdrngo2  37959  isdrngo3  37960  eldmxrncnvepres  38403  eldmxrncnvepres2  38404  prtlem100  38859  prter2  38881  prter3  38882  lsatlspsn2  38992  lsateln0  38995  lsatn0  38999  lsatspn0  39000  lsatcmp  39003  lsatelbN  39006  islshpat  39017  lsat0cv  39033  lkrlspeqN  39171  dvheveccl  41113  dihlatat  41338  dochnel  41394  dihjat1  41430  dvh4dimlem  41444  dochsnkr2cl  41475  dochkr1  41479  dochkr1OLDN  41480  lcfl6lem  41499  lcfl9a  41506  lclkrlem2l  41519  lclkrlem2o  41522  lclkrlem2q  41524  lcfrlem9  41551  lcfrlem16  41559  lcfrlem17  41560  lcfrlem27  41570  lcfrlem37  41580  lcfrlem38  41581  lcfrlem40  41583  lcdlkreqN  41623  mapdrvallem2  41646  mapdn0  41670  mapdpglem20  41692  mapdpglem30  41703  mapdindp0  41720  mapdhcl  41728  mapdh6aN  41736  mapdh6dN  41740  mapdh6eN  41741  mapdh6kN  41747  mapdh8  41789  hdmap1l6a  41810  hdmap1l6d  41814  hdmap1l6e  41815  hdmap1l6k  41821  hdmapval3N  41839  hdmap10  41841  hdmap11lem2  41843  hdmapnzcl  41846  hdmaprnlem3eN  41859  hdmaprnlem17N  41864  hdmap14lem4a  41872  hdmap14lem7  41875  hdmap14lem14  41882  hgmaprnlem5N  41901  hdmaplkr  41914  hdmapip0  41916  hgmapvvlem2  41925  hgmapvvlem3  41926  hgmapvv  41927  redvmptabs  42355  readvrec2  42356  readvrec  42357  fiabv  42531  fsuppind  42585  0prjspnlem  42618  pellexlem5  42828  dfac11  43058  dfacbasgrp  43104  dgraalem  43141  dgraaub  43144  aaitgo  43158  proot1ex  43192  deg1mhm  43196  ofdivrec  44322  ofdivcan4  44323  ofdivdiv2  44324  expgrowth  44331  binomcxplemnotnn0  44352  dvdivbd  45928  dvdivcncf  45932  dirkeritg  46107  fourierdlem39  46151  fourierdlem57  46168  fourierdlem58  46169  fourierdlem59  46170  fourierdlem68  46179  fourierdlem76  46187  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  setsnidel  47382  sprvalpwn0  47488  odz2prm2pw  47568  fmtnoprmfac1  47570  fmtnoprmfac2  47572  sfprmdvdsmersenne  47608  lighneallem2  47611  lighneallem3  47612  lighneal  47616  oddprmALTV  47692  evenprm2  47719  oddprmne2  47720  odd2prm2  47723  even3prm2  47724  isubgruhgr  47872  grimuhgr  47891  2zrngnmrid  48248  lincext1  48447  lindslinindsimp2lem5  48455  rege1logbrege0  48551  fllogbd  48553  relogbmulbexp  48554  relogbdivb  48555  nnpw2blen  48573  blennngt2o2  48585  blennn0e2  48587  dignn0ldlem  48595  line  48725  rrxline  48727  aacllem  49794