Theorem eldifsn 4751

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 4601	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2994	. . 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 2145   ≠ wne 2957   ∖ cdif 3899  {csn 4587

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-sn 4588

This theorem is used by:  eldifsnbd  4752  eldifsnd  4753  eldifsni  4756  rexdifsn  4760  raldifsni  4761  eldifvsn  4763  difsn  4764  sossfld  6183  tpres  7203  onmindif2  7809  xpord3pred  8153  xpord3inddlem  8155  mptsuppd  8188  suppssr  8196  suppssov1  8198  suppssov2  8199  suppsssn  8202  suppssfv  8203  dif1o  8490  difsnen  9060  limenpsi  9153  frfi  9258  fofinf1o  9302  en2eleq  10014  en2other2  10015  dfac8clem  10038  acni2  10052  acndom  10057  acnnum  10058  dfac9  10142  dfacacn  10147  kmlem3  10158  kmlem4  10159  fin23lem21  10344  canthp1lem2  10665  elni  10888  mulnzcnf  11887  divval  11901  elnnne0  12545  elq  13002  rpcndif0  13065  modfzo0difsn  14009  modsumfzodifsn  14010  expcl2lem  14139  expclzlem  14149  hashdifpr  14482  hashgt23el  14491  prprrab  14540  hashle2prv  14545  reccn2  15686  rlimdiv  15735  eff2  16191  tanval  16220  rpnnen2lem9  16314  fzo0dvdseq  16417  oddprmgt2  16794  oddprmdvds  16999  4sqlem19  17059  prmlem0  17201  prmlem1a  17202  setsnid  17304  grpinvnzcl  19135  symgextf  19545  f1omvdmvd  19571  pmtrprfv  19581  odcau  19732  efgsf  19857  efgsrel  19862  efgs1  19863  efgs1b  19864  efgsp1  19865  efgsres  19866  efgredlema  19868  efgredlemd  19872  efgrelexlemb  19878  gsumpt  20090  dmdprdd  20129  dprdcntz  20138  dprdfeq0  20152  dprd2da  20172  domnrrg  20875  isdomn3  20877  drngunit  20896  isdrng2  20907  isdrng3lem2  20916  isdrng5  20918  drngmcl  20919  drngid2  20920  isdrngd  20932  isdrngdOLD  20934  issubdrg  20947  sdrgacs  20968  cntzsdrg  20969  islss  21119  lssneln0  21138  lssssr  21139  lbsind  21265  lbspss  21267  lspabs3  21309  lspsneq  21310  lspfixed  21316  lspexch  21317  islbs2  21342  cnfldinv  21617  cnsubdrglem  21632  cnmgpid  21643  cnmsubglem  21644  gzrngunit  21647  xrs1mnd  21654  xrs10  21655  xrge0subm  21657  zringunit  21680  zringndrg  21682  domnchr  21746  cnmsgngrp  21793  psgninv  21796  psgndiflemB  21814  lindfind  22030  lindsind  22031  lindff1  22034  lindfrn  22035  lindsenlbs  22065  mvrcl  22207  coe1tmmul2  22503  mdetunilem9  22843  maducoeval2  22863  gsummatr01lem4  22881  matunitlindflem2  22903  matunitlindf  22904  ist1-2  23573  cmpfi  23634  2ndcdisj  23683  2ndcsep  23686  locfincmp  23753  alexsublem  24271  cldsubg  24338  imasdsf1olem  24600  prdsxmslem2  24756  reperflem  25046  xrge0gsumle  25061  xrge0tsms  25062  divcn  25097  evth  25188  cvsdiv  25361  cvsdivcl  25362  cphreccllem  25407  bcthlem5  25557  itg11  25920  i1fmullem  25923  i1fadd  25924  itg1addlem2  25926  i1fmulc  25932  itg1mulc  25933  ellimc3  26108  limcmpt2  26113  dvlem  26125  dvidlem  26144  dvcnp  26148  dvcobr  26175  dvrec  26184  dvrecg  26202  dvmptdiv  26203  dvcnvlem  26205  dvexp3  26207  dveflem  26208  dvferm1lem  26213  dvferm2lem  26215  lhop1lem  26242  ftc1lem5  26269  mdegleb  26291  coe1mul3  26326  ply1nz  26349  fta1blem  26398  fta1b  26399  ig1peu  26402  ig1pdvds  26407  plyeq0lem  26437  dgrub  26461  quotval  26523  fta1lem  26538  fta1  26539  elqaalem3  26552  qaa  26554  iaa  26558  aareccl  26559  aannenlem2  26562  abelthlem8  26672  abelth  26674  eff1olem  26783  logrncl  26802  eflog  26811  logeftb  26818  logdmss  26877  dvlog  26886  logbcl  27002  logbid1  27003  logb1  27004  elogb  27005  logbchbase  27006  relogbval  27007  relogbcl  27008  relogbreexp  27010  relogbmul  27012  nnlogbexp  27016  relogbcxp  27020  cxplogb  27021  relogbcxpb  27022  logbf  27024  logblog  27027  2logb9irrALT  27033  sqrt2cxp2logb9e3  27034  angval  27036  dcubic  27081  rlimcnp  27200  efrlim  27204  logexprlim  27459  dchrghm  27490  dchrabs  27494  lgsfcl2  27537  lgsval2lem  27541  lgsval3  27549  lgsmod  27557  lgsdirprm  27565  lgsne0  27569  gausslemma2dlem0f  27595  lgsquad2lem2  27619  2lgsoddprm  27650  2sqlem11  27663  2sqblem  27665  dchrvmaeq0  27738  rpvmasum2  27746  dchrisum0re  27747  qrngdiv  27858  addsval  28225  divsval  28452  elnns  28603  1nns  28612  tglngval  28891  tgisline  28972  axlowdimlem9  29393  axlowdimlem12  29396  axlowdimlem13  29397  elntg2  29428  upgrbi  29536  upgr1elem  29555  umgrislfupgrlem  29565  edgupgr  29577  subgruhgredgd  29730  upgrreslem  29750  nbgrel  29786  nbupgr  29790  nbupgrel  29791  nbumgrvtx  29792  nbgrssovtx  29807  nbupgrres  29810  nbusgrvtxm1uvtx  29851  nbupgruvtxres  29853  iscplgredg  29863  cusgredg  29870  cusgrfilem2  29902  usgredgsscusgredg  29905  1loopgrnb0  29948  1egrvtxdg0  29957  uhgrvd00  29980  vtxdginducedm1lem4  29988  eupth2lem3lem3  30696  frcond1  30732  frcond4  30736  2pthfrgr  30750  3cyclfrgrrn1  30751  n4cyclfrgr  30757  frgrwopreglem4a  30776  numclwwlk5  30854  ressupprn  33149  suppss3  33181  xdivval  33351  xrge0tsmsd  33500  pmtrcnel  33516  pmtrcnelor  33518  0nellinds  33792  dvdsruasso  33805  extdg1id  34163  irngnzply1  34188  submatminr1  34307  ordtconnlem1  34421  ispisys2  34651  sigapisys  34653  sibfinima  34837  sseqf  34890  signswch  35056  signstfvn  35064  signsvtn0  35065  signstfvneq0  35067  signstfvcl  35068  signstfveq0a  35071  signstfveq0  35072  signsvfn  35077  signsvtp  35078  signsvtn  35079  signsvfpn  35080  signsvfnn  35081  signlem0  35082  bnj158  35226  bnj168  35227  bnj529  35238  bnj906  35426  bnj970  35443  exdifsn  35576  cusgredgex2  35708  subfacp1lem5  35750  cvmsi  35831  cvmsval  35832  cvmsdisj  35836  cvmscld  35839  cvmsss2  35840  satfv1lem  35928  sinccvglem  36238  circum  36240  mpomulnzcnf  36906  unbdqndv2lem2  37194  bj-0int  37838  lindsadd  38354  poimirlem6  38362  poimirlem7  38363  poimirlem8  38364  poimirlem16  38372  poimirlem18  38374  poimirlem19  38375  poimirlem21  38377  poimirlem22  38378  poimirlem24  38380  poimirlem25  38381  poimirlem26  38382  poimirlem27  38383  itg2addnclem2  38408  sdclem1  38480  rrncmslem  38569  rrnequiv  38572  isdrngo2  38695  isdrngo3  38696  eldmxrncnvepres  39169  eldmxrncnvepres2  39170  prtlem100  39719  prter2  39741  prter3  39742  lsatlspsn2  39852  lsateln0  39855  lsatn0  39859  lsatspn0  39860  lsatcmp  39863  lsatelbN  39866  islshpat  39877  lsat0cv  39893  lkrlspeqN  40031  dvheveccl  41972  dihlatat  42197  dochnel  42253  dihjat1  42289  dvh4dimlem  42303  dochsnkr2cl  42334  dochkr1  42338  dochkr1OLDN  42339  lcfl6lem  42358  lcfl9a  42365  lclkrlem2l  42378  lclkrlem2o  42381  lclkrlem2q  42383  lcfrlem9  42410  lcfrlem16  42418  lcfrlem17  42419  lcfrlem27  42429  lcfrlem37  42439  lcfrlem38  42440  lcfrlem40  42442  lcdlkreqN  42482  mapdrvallem2  42505  mapdn0  42529  mapdpglem20  42551  mapdpglem30  42562  mapdindp0  42579  mapdhcl  42587  mapdh6aN  42595  mapdh6dN  42599  mapdh6eN  42600  mapdh6kN  42606  mapdh8  42648  hdmap1l6a  42669  hdmap1l6d  42673  hdmap1l6e  42674  hdmap1l6k  42680  hdmapval3N  42698  hdmap10  42700  hdmap11lem2  42702  hdmapnzcl  42705  hdmaprnlem3eN  42718  hdmaprnlem17N  42723  hdmap14lem4a  42731  hdmap14lem7  42734  hdmap14lem14  42741  hgmaprnlem5N  42760  hdmaplkr  42773  hdmapip0  42775  hgmapvvlem2  42784  hgmapvvlem3  42785  hgmapvv  42786  redvmptabs  43222  readvrec2  43223  readvrec  43224  fiabv  43405  fsuppind  43423  0prjspnlem  43456  pellexlem5  43661  dfac11  43890  dfacbasgrp  43936  dgraalem  43973  dgraaub  43976  aaitgo  43990  proot1ex  44024  deg1mhm  44028  ofdivrec  45137  ofdivcan4  45138  ofdivdiv2  45139  expgrowth  45146  binomcxplemnotnn0  45167  dvdivbd  46738  dvdivcncf  46742  dirkeritg  46917  fourierdlem39  46961  fourierdlem57  46978  fourierdlem58  46979  fourierdlem59  46980  fourierdlem68  46989  fourierdlem76  46997  fourierdlem103  47024  fourierdlem104  47025  fourierdlem111  47032  setsnidel  48264  sprvalpwn0  48370  odz2prm2pw  48453  fmtnoprmfac1  48455  fmtnoprmfac2  48457  sfprmdvdsmersenne  48493  lighneallem2  48496  lighneallem3  48497  lighneal  48501  oddprmALTV  48590  evenprm2  48617  oddprmne2  48618  odd2prm2  48621  even3prm2  48622  isubgruhgr  48771  grimuhgr  48790  2zrngnmrid  49158  lincext1  49371  lindslinindsimp2lem5  49379  rege1logbrege0  49475  fllogbd  49477  relogbmulbexp  49478  relogbdivb  49479  nnpw2blen  49497  blennngt2o2  49509  blennn0e2  49511  dignn0ldlem  49519  line  49649  rrxline  49651  dvsec  50676  dvcsc  50677  dvcot  50678  aacllem  50759  veroquadmodzerod  50804  veroquadnolindfd  50805