Theorem eldifsn 4783

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 3954	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4636	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2977	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 575	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 274	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   ∈ wcel 2106   ≠ wne 2939   ∖ cdif 3941  {csn 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-v 3475  df-dif 3947  df-sn 4623

This theorem is referenced by:  elpwdifsn  4785  eldifsni  4786  rexdifsn  4790  raldifsni  4791  eldifvsn  4793  difsn  4794  prproe  4899  sossfld  6174  tpres  7186  onmindif2  7778  xpord3pred  8120  xpord3inddlem  8122  mptsuppd  8154  suppssr  8163  suppssov1  8165  suppsssn  8168  suppssfv  8169  dif1o  8482  difsnen  9036  limenpsi  9135  frfi  9271  fofinf1o  9310  en2eleq  9985  en2other2  9986  dfac8clem  10009  acni2  10023  acndom  10028  acnnum  10029  dfac9  10113  dfacacn  10118  kmlem3  10129  kmlem4  10130  fin23lem21  10316  canthp1lem2  10630  elni  10853  mulnzcnopr  11842  divval  11856  elnnne0  12468  elq  12916  rpcndif0  12975  modfzo0difsn  13890  modsumfzodifsn  13891  expcl2lem  14021  expclzlem  14031  hashdifpr  14357  hashgt23el  14366  prprrab  14416  hashle2prv  14421  reccn2  15523  rlimdiv  15574  eff2  16024  tanval  16053  rpnnen2lem9  16147  fzo0dvdseq  16248  oddprmgt2  16618  oddprmdvds  16818  4sqlem19  16878  prmlem0  17021  prmlem1a  17022  setsnid  17124  setsnidOLD  17125  grpinvnzcl  18869  symgextf  19249  f1omvdmvd  19275  pmtrprfv  19285  odcau  19436  efgsf  19561  efgsrel  19566  efgs1  19567  efgs1b  19568  efgsp1  19569  efgsres  19570  efgredlema  19572  efgredlemd  19576  efgrelexlemb  19582  gsumpt  19789  dmdprdd  19828  dprdcntz  19837  dprdfeq0  19851  dprd2da  19871  drngunit  20270  isdrng2  20278  drngid2  20285  isdrngd  20297  isdrngdOLD  20299  issubdrg  20338  sdrgacs  20366  cntzsdrg  20367  abvtriv  20398  islss  20494  lssneln0  20512  lssssr  20513  lbsind  20640  lbspss  20642  lspabs3  20683  lspsneq  20684  lspfixed  20690  lspexch  20691  islbs2  20716  isdomn2  20851  domnrrg  20852  cnflddiv  20909  cnfldinv  20910  xrs1mnd  20917  xrs10  20918  xrge0subm  20920  cnsubdrglem  20930  cnmgpid  20941  cnmsubglem  20942  gzrngunit  20945  zringunit  20969  zringndrg  20971  domnchr  21017  cnmsgngrp  21065  psgninv  21068  psgndiflemB  21086  lindfind  21304  lindsind  21305  lindff1  21308  lindfrn  21309  mvrcl  21503  coe1tmmul2  21729  mdetunilem9  22051  maducoeval2  22071  gsummatr01lem4  22089  ist1-2  22780  cmpfi  22841  2ndcdisj  22889  2ndcsep  22892  locfincmp  22959  alexsublem  23477  cldsubg  23544  imasdsf1olem  23808  prdsxmslem2  23967  reperflem  24263  xrge0gsumle  24278  xrge0tsms  24279  divcn  24313  evth  24404  cvsdiv  24577  cvsdivcl  24578  cphreccllem  24624  bcthlem5  24774  itg11  25137  i1fmullem  25140  i1fadd  25141  itg1addlem2  25143  i1fmulc  25150  itg1mulc  25151  ellimc3  25325  limcmpt2  25330  dvlem  25342  dvidlem  25361  dvcnp  25365  dvcobr  25392  dvrec  25401  dvrecg  25419  dvmptdiv  25420  dvcnvlem  25422  dvexp3  25424  dveflem  25425  dvferm1lem  25430  dvferm2lem  25432  lhop1lem  25459  ftc1lem5  25486  mdegleb  25511  coe1mul3  25546  ply1nz  25568  fta1blem  25615  fta1b  25616  ig1peu  25618  ig1pdvds  25623  plyeq0lem  25653  dgrub  25677  quotval  25734  fta1lem  25749  fta1  25750  elqaalem3  25763  qaa  25765  iaa  25767  aareccl  25768  aannenlem2  25771  abelthlem8  25880  abelth  25882  eff1olem  25986  logrncl  26005  eflog  26014  logeftb  26021  logdmss  26079  dvlog  26088  logbcl  26199  logbid1  26200  logb1  26201  elogb  26202  logbchbase  26203  relogbval  26204  relogbcl  26205  relogbreexp  26207  relogbmul  26209  nnlogbexp  26213  relogbcxp  26217  cxplogb  26218  relogbcxpb  26219  logbf  26221  logblog  26224  2logb9irrALT  26230  sqrt2cxp2logb9e3  26231  angval  26233  dcubic  26278  rlimcnp  26397  efrlim  26401  logexprlim  26655  dchrghm  26686  dchrabs  26690  lgsfcl2  26733  lgsval2lem  26737  lgsval3  26745  lgsmod  26753  lgsdirprm  26761  lgsne0  26765  gausslemma2dlem0f  26791  lgsquad2lem2  26815  2lgsoddprm  26846  2sqlem11  26859  2sqblem  26861  dchrvmaeq0  26934  rpvmasum2  26942  dchrisum0re  26943  qrngdiv  27054  addsval  27362  tglngval  27667  tgisline  27743  axlowdimlem9  28073  axlowdimlem12  28076  axlowdimlem13  28077  elntg2  28108  upgrbi  28218  upgr1elem  28237  umgrislfupgrlem  28247  edgupgr  28259  subgruhgredgd  28406  upgrreslem  28426  nbgrel  28462  nbupgr  28466  nbupgrel  28467  nbumgrvtx  28468  nbgrssovtx  28483  nbupgrres  28486  nbusgrvtxm1uvtx  28527  nbupgruvtxres  28529  iscplgredg  28539  cusgredg  28546  cusgrfilem2  28578  usgredgsscusgredg  28581  1loopgrnb0  28624  1egrvtxdg0  28633  uhgrvd00  28656  vtxdginducedm1lem4  28664  eupth2lem3lem3  29348  frcond1  29384  frcond4  29388  2pthfrgr  29402  3cyclfrgrrn1  29403  n4cyclfrgr  29409  frgrwopreglem4a  29428  numclwwlk5  29506  ressupprn  31783  suppss3  31820  xdivval  31956  xrge0tsmsd  32080  pmtrcnel  32121  pmtrcnelor  32123  0nellinds  32345  extdg1id  32580  irngnzply1  32593  submatminr1  32621  ordtconnlem1  32735  ispisys2  32982  sigapisys  32984  sibfinima  33169  sseqf  33222  signswch  33403  signstfvn  33411  signsvtn0  33412  signstfvneq0  33414  signstfvcl  33415  signstfveq0a  33418  signstfveq0  33419  signsvfn  33424  signsvtp  33425  signsvtn  33426  signsvfpn  33427  signsvfnn  33428  signlem0  33429  bnj158  33571  bnj168  33572  bnj529  33583  bnj906  33772  bnj970  33789  exdifsn  33915  cusgredgex2  33944  subfacp1lem5  34006  cvmsi  34087  cvmsval  34088  cvmsdisj  34092  cvmscld  34095  cvmsss2  34096  satfv1lem  34184  sinccvglem  34488  circum  34490  unbdqndv2lem2  35190  bj-0int  35786  lindsadd  36285  lindsenlbs  36287  matunitlindflem2  36289  matunitlindf  36290  poimirlem6  36298  poimirlem7  36299  poimirlem8  36300  poimirlem16  36308  poimirlem18  36310  poimirlem19  36311  poimirlem21  36313  poimirlem22  36314  poimirlem24  36316  poimirlem25  36317  poimirlem26  36318  poimirlem27  36319  itg2addnclem2  36344  sdclem1  36416  rrncmslem  36505  rrnequiv  36508  isdrngo2  36631  isdrngo3  36632  prtlem100  37534  prter2  37556  prter3  37557  lsatlspsn2  37667  lsateln0  37670  lsatn0  37674  lsatspn0  37675  lsatcmp  37678  lsatelbN  37681  islshpat  37692  lsat0cv  37708  lkrlspeqN  37846  dvheveccl  39788  dihlatat  40013  dochnel  40069  dihjat1  40105  dvh4dimlem  40119  dochsnkr2cl  40150  dochkr1  40154  dochkr1OLDN  40155  lcfl6lem  40174  lcfl9a  40181  lclkrlem2l  40194  lclkrlem2o  40197  lclkrlem2q  40199  lcfrlem9  40226  lcfrlem16  40234  lcfrlem17  40235  lcfrlem27  40245  lcfrlem37  40255  lcfrlem38  40256  lcfrlem40  40258  lcdlkreqN  40298  mapdrvallem2  40321  mapdn0  40345  mapdpglem20  40367  mapdpglem30  40378  mapdindp0  40395  mapdhcl  40403  mapdh6aN  40411  mapdh6dN  40415  mapdh6eN  40416  mapdh6kN  40422  mapdh8  40464  hdmap1l6a  40485  hdmap1l6d  40489  hdmap1l6e  40490  hdmap1l6k  40496  hdmapval3N  40514  hdmap10  40516  hdmap11lem2  40518  hdmapnzcl  40521  hdmaprnlem3eN  40534  hdmaprnlem17N  40539  hdmap14lem4a  40547  hdmap14lem7  40550  hdmap14lem14  40557  hgmaprnlem5N  40576  hdmaplkr  40589  hdmapip0  40591  hgmapvvlem2  40600  hgmapvvlem3  40601  hgmapvv  40602  fsuppind  40951  0prjspnlem  41147  pellexlem5  41342  dfac11  41575  dfacbasgrp  41621  dgraalem  41658  dgraaub  41661  aaitgo  41675  proot1ex  41714  isdomn3  41717  deg1mhm  41720  ofdivrec  42856  ofdivcan4  42857  ofdivdiv2  42858  expgrowth  42865  binomcxplemnotnn0  42886  dvdivbd  44412  dvdivcncf  44416  dirkeritg  44591  fourierdlem39  44635  fourierdlem57  44652  fourierdlem58  44653  fourierdlem59  44654  fourierdlem68  44663  fourierdlem76  44671  fourierdlem103  44698  fourierdlem104  44699  fourierdlem111  44706  setsnidel  45817  sprvalpwn0  45923  odz2prm2pw  46003  fmtnoprmfac1  46005  fmtnoprmfac2  46007  sfprmdvdsmersenne  46043  lighneallem2  46046  lighneallem3  46047  lighneal  46051  oddprmALTV  46127  evenprm2  46154  oddprmne2  46155  odd2prm2  46158  even3prm2  46159  2zrngnmrid  46496  lincext1  46783  lindslinindsimp2lem5  46791  rege1logbrege0  46892  fllogbd  46894  relogbmulbexp  46895  relogbdivb  46896  nnpw2blen  46914  blennngt2o2  46926  blennn0e2  46928  dignn0ldlem  46936  line  47066  rrxline  47068  aacllem  47496