Theorem eldifsn 4791

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 397   ∈ wcel 2107   ≠ wne 2941   ∖ cdif 3946  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-sn 4630

This theorem is referenced by:  elpwdifsn  4793  eldifsni  4794  rexdifsn  4798  raldifsni  4799  eldifvsn  4801  difsn  4802  prproe  4907  sossfld  6186  tpres  7202  onmindif2  7795  xpord3pred  8138  xpord3inddlem  8140  mptsuppd  8172  suppssr  8181  suppssov1  8183  suppsssn  8186  suppssfv  8187  dif1o  8500  difsnen  9053  limenpsi  9152  frfi  9288  fofinf1o  9327  en2eleq  10003  en2other2  10004  dfac8clem  10027  acni2  10041  acndom  10046  acnnum  10047  dfac9  10131  dfacacn  10136  kmlem3  10147  kmlem4  10148  fin23lem21  10334  canthp1lem2  10648  elni  10871  mulnzcnopr  11860  divval  11874  elnnne0  12486  elq  12934  rpcndif0  12993  modfzo0difsn  13908  modsumfzodifsn  13909  expcl2lem  14039  expclzlem  14049  hashdifpr  14375  hashgt23el  14384  prprrab  14434  hashle2prv  14439  reccn2  15541  rlimdiv  15592  eff2  16042  tanval  16071  rpnnen2lem9  16165  fzo0dvdseq  16266  oddprmgt2  16636  oddprmdvds  16836  4sqlem19  16896  prmlem0  17039  prmlem1a  17040  setsnid  17142  setsnidOLD  17143  grpinvnzcl  18895  symgextf  19285  f1omvdmvd  19311  pmtrprfv  19321  odcau  19472  efgsf  19597  efgsrel  19602  efgs1  19603  efgs1b  19604  efgsp1  19605  efgsres  19606  efgredlema  19608  efgredlemd  19612  efgrelexlemb  19618  gsumpt  19830  dmdprdd  19869  dprdcntz  19878  dprdfeq0  19892  dprd2da  19912  drngunit  20362  isdrng2  20371  drngid2  20378  isdrngd  20390  isdrngdOLD  20392  issubdrg  20401  sdrgacs  20417  cntzsdrg  20418  abvtriv  20449  islss  20545  lssneln0  20563  lssssr  20564  lbsind  20691  lbspss  20693  lspabs3  20734  lspsneq  20735  lspfixed  20741  lspexch  20742  islbs2  20767  isdomn2  20915  domnrrg  20916  cnflddiv  20975  cnfldinv  20976  xrs1mnd  20983  xrs10  20984  xrge0subm  20986  cnsubdrglem  20996  cnmgpid  21007  cnmsubglem  21008  gzrngunit  21011  zringunit  21036  zringndrg  21038  domnchr  21084  cnmsgngrp  21132  psgninv  21135  psgndiflemB  21153  lindfind  21371  lindsind  21372  lindff1  21375  lindfrn  21376  mvrcl  21551  coe1tmmul2  21798  mdetunilem9  22122  maducoeval2  22142  gsummatr01lem4  22160  ist1-2  22851  cmpfi  22912  2ndcdisj  22960  2ndcsep  22963  locfincmp  23030  alexsublem  23548  cldsubg  23615  imasdsf1olem  23879  prdsxmslem2  24038  reperflem  24334  xrge0gsumle  24349  xrge0tsms  24350  divcn  24384  evth  24475  cvsdiv  24648  cvsdivcl  24649  cphreccllem  24695  bcthlem5  24845  itg11  25208  i1fmullem  25211  i1fadd  25212  itg1addlem2  25214  i1fmulc  25221  itg1mulc  25222  ellimc3  25396  limcmpt2  25401  dvlem  25413  dvidlem  25432  dvcnp  25436  dvcobr  25463  dvrec  25472  dvrecg  25490  dvmptdiv  25491  dvcnvlem  25493  dvexp3  25495  dveflem  25496  dvferm1lem  25501  dvferm2lem  25503  lhop1lem  25530  ftc1lem5  25557  mdegleb  25582  coe1mul3  25617  ply1nz  25639  fta1blem  25686  fta1b  25687  ig1peu  25689  ig1pdvds  25694  plyeq0lem  25724  dgrub  25748  quotval  25805  fta1lem  25820  fta1  25821  elqaalem3  25834  qaa  25836  iaa  25838  aareccl  25839  aannenlem2  25842  abelthlem8  25951  abelth  25953  eff1olem  26057  logrncl  26076  eflog  26085  logeftb  26092  logdmss  26150  dvlog  26159  logbcl  26272  logbid1  26273  logb1  26274  elogb  26275  logbchbase  26276  relogbval  26277  relogbcl  26278  relogbreexp  26280  relogbmul  26282  nnlogbexp  26286  relogbcxp  26290  cxplogb  26291  relogbcxpb  26292  logbf  26294  logblog  26297  2logb9irrALT  26303  sqrt2cxp2logb9e3  26304  angval  26306  dcubic  26351  rlimcnp  26470  efrlim  26474  logexprlim  26728  dchrghm  26759  dchrabs  26763  lgsfcl2  26806  lgsval2lem  26810  lgsval3  26818  lgsmod  26826  lgsdirprm  26834  lgsne0  26838  gausslemma2dlem0f  26864  lgsquad2lem2  26888  2lgsoddprm  26919  2sqlem11  26932  2sqblem  26934  dchrvmaeq0  27007  rpvmasum2  27015  dchrisum0re  27016  qrngdiv  27127  addsval  27446  divsval  27637  tglngval  27802  tgisline  27878  axlowdimlem9  28208  axlowdimlem12  28211  axlowdimlem13  28212  elntg2  28243  upgrbi  28353  upgr1elem  28372  umgrislfupgrlem  28382  edgupgr  28394  subgruhgredgd  28541  upgrreslem  28561  nbgrel  28597  nbupgr  28601  nbupgrel  28602  nbumgrvtx  28603  nbgrssovtx  28618  nbupgrres  28621  nbusgrvtxm1uvtx  28662  nbupgruvtxres  28664  iscplgredg  28674  cusgredg  28681  cusgrfilem2  28713  usgredgsscusgredg  28716  1loopgrnb0  28759  1egrvtxdg0  28768  uhgrvd00  28791  vtxdginducedm1lem4  28799  eupth2lem3lem3  29483  frcond1  29519  frcond4  29523  2pthfrgr  29537  3cyclfrgrrn1  29538  n4cyclfrgr  29544  frgrwopreglem4a  29563  numclwwlk5  29641  ressupprn  31912  suppss3  31949  xdivval  32085  xrge0tsmsd  32209  pmtrcnel  32250  pmtrcnelor  32252  0nellinds  32483  dvdsruasso  32490  mxidlirredi  32587  extdg1id  32742  irngnzply1  32755  submatminr1  32790  ordtconnlem1  32904  ispisys2  33151  sigapisys  33153  sibfinima  33338  sseqf  33391  signswch  33572  signstfvn  33580  signsvtn0  33581  signstfvneq0  33583  signstfvcl  33584  signstfveq0a  33587  signstfveq0  33588  signsvfn  33593  signsvtp  33594  signsvtn  33595  signsvfpn  33596  signsvfnn  33597  signlem0  33598  bnj158  33740  bnj168  33741  bnj529  33752  bnj906  33941  bnj970  33958  exdifsn  34084  cusgredgex2  34113  subfacp1lem5  34175  cvmsi  34256  cvmsval  34257  cvmsdisj  34261  cvmscld  34264  cvmsss2  34265  satfv1lem  34353  sinccvglem  34657  circum  34659  gg-divcn  35163  gg-dvcobr  35176  unbdqndv2lem2  35386  bj-0int  35982  lindsadd  36481  lindsenlbs  36483  matunitlindflem2  36485  matunitlindf  36486  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem16  36504  poimirlem18  36506  poimirlem19  36507  poimirlem21  36509  poimirlem22  36510  poimirlem24  36512  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  itg2addnclem2  36540  sdclem1  36611  rrncmslem  36700  rrnequiv  36703  isdrngo2  36826  isdrngo3  36827  prtlem100  37729  prter2  37751  prter3  37752  lsatlspsn2  37862  lsateln0  37865  lsatn0  37869  lsatspn0  37870  lsatcmp  37873  lsatelbN  37876  islshpat  37887  lsat0cv  37903  lkrlspeqN  38041  dvheveccl  39983  dihlatat  40208  dochnel  40264  dihjat1  40300  dvh4dimlem  40314  dochsnkr2cl  40345  dochkr1  40349  dochkr1OLDN  40350  lcfl6lem  40369  lcfl9a  40376  lclkrlem2l  40389  lclkrlem2o  40392  lclkrlem2q  40394  lcfrlem9  40421  lcfrlem16  40429  lcfrlem17  40430  lcfrlem27  40440  lcfrlem37  40450  lcfrlem38  40451  lcfrlem40  40453  lcdlkreqN  40493  mapdrvallem2  40516  mapdn0  40540  mapdpglem20  40562  mapdpglem30  40573  mapdindp0  40590  mapdhcl  40598  mapdh6aN  40606  mapdh6dN  40610  mapdh6eN  40611  mapdh6kN  40617  mapdh8  40659  hdmap1l6a  40680  hdmap1l6d  40684  hdmap1l6e  40685  hdmap1l6k  40691  hdmapval3N  40709  hdmap10  40711  hdmap11lem2  40713  hdmapnzcl  40716  hdmaprnlem3eN  40729  hdmaprnlem17N  40734  hdmap14lem4a  40742  hdmap14lem7  40745  hdmap14lem14  40752  hgmaprnlem5N  40771  hdmaplkr  40784  hdmapip0  40786  hgmapvvlem2  40795  hgmapvvlem3  40796  hgmapvv  40797  fsuppind  41162  0prjspnlem  41365  pellexlem5  41571  dfac11  41804  dfacbasgrp  41850  dgraalem  41887  dgraaub  41890  aaitgo  41904  proot1ex  41943  isdomn3  41946  deg1mhm  41949  ofdivrec  43085  ofdivcan4  43086  ofdivdiv2  43087  expgrowth  43094  binomcxplemnotnn0  43115  dvdivbd  44639  dvdivcncf  44643  dirkeritg  44818  fourierdlem39  44862  fourierdlem57  44879  fourierdlem58  44880  fourierdlem59  44881  fourierdlem68  44890  fourierdlem76  44898  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  setsnidel  46045  sprvalpwn0  46151  odz2prm2pw  46231  fmtnoprmfac1  46233  fmtnoprmfac2  46235  sfprmdvdsmersenne  46271  lighneallem2  46274  lighneallem3  46275  lighneal  46279  oddprmALTV  46355  evenprm2  46382  oddprmne2  46383  odd2prm2  46386  even3prm2  46387  2zrngnmrid  46848  lincext1  47135  lindslinindsimp2lem5  47143  rege1logbrege0  47244  fllogbd  47246  relogbmulbexp  47247  relogbdivb  47248  nnpw2blen  47266  blennngt2o2  47278  blennn0e2  47280  dignn0ldlem  47288  line  47418  rrxline  47420  aacllem  47848