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 3916	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4598	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2996	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 582	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 277	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399   ∈ wcel 2144   ≠ wne 2959   ∖ cdif 3903  {csn 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-v 3458  df-dif 3909  df-sn 4585

This theorem is referenced by:  eldifsnd  4749  eldifsni  4752  rexdifsn  4756  raldifsni  4757  eldifvsn  4759  difsn  4760  sossfld  6174  tpres  7187  onmindif2  7792  xpord3pred  8134  xpord3inddlem  8136  mptsuppd  8169  suppssr  8177  suppssov1  8179  suppssov2  8180  suppsssn  8183  suppssfv  8184  dif1o  8471  difsnen  9033  limenpsi  9126  frfi  9231  fofinf1o  9277  en2eleq  9966  en2other2  9967  dfac8clem  9990  acni2  10004  acndom  10009  acnnum  10010  dfac9  10095  dfacacn  10100  kmlem3  10111  kmlem4  10112  fin23lem21  10298  canthp1lem2  10613  elni  10836  mulnzcnf  11835  divval  11849  elnnne0  12497  elq  12953  rpcndif0  13016  modfzo0difsn  13958  modsumfzodifsn  13959  expcl2lem  14088  expclzlem  14098  hashdifpr  14430  hashgt23el  14439  prprrab  14488  hashle2prv  14493  reccn2  15626  rlimdiv  15675  eff2  16133  tanval  16162  rpnnen2lem9  16256  fzo0dvdseq  16359  oddprmgt2  16736  oddprmdvds  16941  4sqlem19  17001  prmlem0  17143  prmlem1a  17144  setsnid  17246  grpinvnzcl  19055  symgextf  19459  f1omvdmvd  19485  pmtrprfv  19495  odcau  19646  efgsf  19771  efgsrel  19776  efgs1  19777  efgs1b  19778  efgsp1  19779  efgsres  19780  efgredlema  19782  efgredlemd  19786  efgrelexlemb  19792  gsumpt  20004  dmdprdd  20043  dprdcntz  20052  dprdfeq0  20066  dprd2da  20086  isdomn2OLD  20764  domnrrg  20765  isdomn3  20767  drngunit  20786  isdrng2  20795  drngmcl  20802  drngid2  20804  isdrngd  20817  isdrngdOLD  20819  issubdrg  20831  sdrgacs  20852  cntzsdrg  20853  islss  21003  lssneln0  21022  lssssr  21023  lbsind  21149  lbspss  21151  lspabs3  21193  lspsneq  21194  lspfixed  21200  lspexch  21201  islbs2  21226  cnfldinv  21457  cnsubdrglem  21472  cnmgpid  21483  cnmsubglem  21484  gzrngunit  21487  xrs1mnd  21494  xrs10  21495  xrge0subm  21497  zringunit  21520  zringndrg  21522  domnchr  21586  cnmsgngrp  21633  psgninv  21636  psgndiflemB  21654  lindfind  21870  lindsind  21871  lindff1  21874  lindfrn  21875  mvrcl  22045  coe1tmmul2  22341  mdetunilem9  22682  maducoeval2  22702  gsummatr01lem4  22720  ist1-2  23409  cmpfi  23470  2ndcdisj  23518  2ndcsep  23521  locfincmp  23588  alexsublem  24106  cldsubg  24173  imasdsf1olem  24435  prdsxmslem2  24591  reperflem  24881  xrge0gsumle  24896  xrge0tsms  24897  divcn  24932  evth  25023  cvsdiv  25196  cvsdivcl  25197  cphreccllem  25242  bcthlem5  25392  itg11  25755  i1fmullem  25758  i1fadd  25759  itg1addlem2  25761  i1fmulc  25767  itg1mulc  25768  ellimc3  25943  limcmpt2  25948  dvlem  25960  dvidlem  25979  dvcnp  25983  dvcobr  26010  dvrec  26019  dvrecg  26037  dvmptdiv  26038  dvcnvlem  26040  dvexp3  26042  dveflem  26043  dvferm1lem  26048  dvferm2lem  26050  lhop1lem  26077  ftc1lem5  26104  mdegleb  26126  coe1mul3  26161  ply1nz  26184  fta1blem  26233  fta1b  26234  ig1peu  26237  ig1pdvds  26242  plyeq0lem  26272  dgrub  26296  quotval  26358  fta1lem  26373  fta1  26374  elqaalem3  26387  qaa  26389  iaa  26391  aareccl  26392  aannenlem2  26395  abelthlem8  26504  abelth  26506  eff1olem  26615  logrncl  26634  eflog  26643  logeftb  26650  logdmss  26709  dvlog  26718  logbcl  26834  logbid1  26835  logb1  26836  elogb  26837  logbchbase  26838  relogbval  26839  relogbcl  26840  relogbreexp  26842  relogbmul  26844  nnlogbexp  26848  relogbcxp  26852  cxplogb  26853  relogbcxpb  26854  logbf  26856  logblog  26859  2logb9irrALT  26865  sqrt2cxp2logb9e3  26866  angval  26868  dcubic  26913  rlimcnp  27032  efrlim  27036  logexprlim  27291  dchrghm  27322  dchrabs  27326  lgsfcl2  27369  lgsval2lem  27373  lgsval3  27381  lgsmod  27389  lgsdirprm  27397  lgsne0  27401  gausslemma2dlem0f  27427  lgsquad2lem2  27451  2lgsoddprm  27482  2sqlem11  27495  2sqblem  27497  dchrvmaeq0  27570  rpvmasum2  27578  dchrisum0re  27579  qrngdiv  27690  addsval  28057  divsval  28284  elnns  28435  1nns  28444  tglngval  28722  tgisline  28798  axlowdimlem9  29153  axlowdimlem12  29156  axlowdimlem13  29157  elntg2  29188  upgrbi  29296  upgr1elem  29315  umgrislfupgrlem  29325  edgupgr  29337  subgruhgredgd  29487  upgrreslem  29507  nbgrel  29543  nbupgr  29547  nbupgrel  29548  nbumgrvtx  29549  nbgrssovtx  29564  nbupgrres  29567  nbusgrvtxm1uvtx  29608  nbupgruvtxres  29610  iscplgredg  29620  cusgredg  29627  cusgrfilem2  29659  usgredgsscusgredg  29662  1loopgrnb0  29705  1egrvtxdg0  29714  uhgrvd00  29737  vtxdginducedm1lem4  29745  eupth2lem3lem3  30434  frcond1  30470  frcond4  30474  2pthfrgr  30488  3cyclfrgrrn1  30489  n4cyclfrgr  30495  frgrwopreglem4a  30514  numclwwlk5  30592  ressupprn  32894  suppss3  32927  xdivval  33098  xrge0tsmsd  33255  pmtrcnel  33271  pmtrcnelor  33273  0nellinds  33558  dvdsruasso  33573  extdg1id  33965  irngnzply1  33990  submatminr1  34109  ordtconnlem1  34223  ispisys2  34452  sigapisys  34454  sibfinima  34638  sseqf  34691  signswch  34857  signstfvn  34865  signsvtn0  34866  signstfvneq0  34868  signstfvcl  34869  signstfveq0a  34872  signstfveq0  34873  signsvfn  34878  signsvtp  34879  signsvtn  34880  signsvfpn  34881  signsvfnn  34882  signlem0  34883  bnj158  35027  bnj168  35028  bnj529  35039  bnj906  35227  bnj970  35244  exdifsn  35376  cusgredgex2  35478  subfacp1lem5  35539  cvmsi  35620  cvmsval  35621  cvmsdisj  35625  cvmscld  35628  cvmsss2  35629  satfv1lem  35717  sinccvglem  36027  circum  36029  mpomulnzcnf  36664  unbdqndv2lem2  36953  bj-0int  37596  lindsadd  38117  lindsenlbs  38119  matunitlindflem2  38121  matunitlindf  38122  poimirlem6  38130  poimirlem7  38131  poimirlem8  38132  poimirlem16  38140  poimirlem18  38142  poimirlem19  38143  poimirlem21  38145  poimirlem22  38146  poimirlem24  38148  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  itg2addnclem2  38176  sdclem1  38247  rrncmslem  38336  rrnequiv  38339  isdrngo2  38462  isdrngo3  38463  eldmxrncnvepres  38938  eldmxrncnvepres2  38939  prtlem100  39488  prter2  39510  prter3  39511  lsatlspsn2  39621  lsateln0  39624  lsatn0  39628  lsatspn0  39629  lsatcmp  39632  lsatelbN  39635  islshpat  39646  lsat0cv  39662  lkrlspeqN  39800  dvheveccl  41741  dihlatat  41966  dochnel  42022  dihjat1  42058  dvh4dimlem  42072  dochsnkr2cl  42103  dochkr1  42107  dochkr1OLDN  42108  lcfl6lem  42127  lcfl9a  42134  lclkrlem2l  42147  lclkrlem2o  42150  lclkrlem2q  42152  lcfrlem9  42179  lcfrlem16  42187  lcfrlem17  42188  lcfrlem27  42198  lcfrlem37  42208  lcfrlem38  42209  lcfrlem40  42211  lcdlkreqN  42251  mapdrvallem2  42274  mapdn0  42298  mapdpglem20  42320  mapdpglem30  42331  mapdindp0  42348  mapdhcl  42356  mapdh6aN  42364  mapdh6dN  42368  mapdh6eN  42369  mapdh6kN  42375  mapdh8  42417  hdmap1l6a  42438  hdmap1l6d  42442  hdmap1l6e  42443  hdmap1l6k  42449  hdmapval3N  42467  hdmap10  42469  hdmap11lem2  42471  hdmapnzcl  42474  hdmaprnlem3eN  42487  hdmaprnlem17N  42492  hdmap14lem4a  42500  hdmap14lem7  42503  hdmap14lem14  42510  hgmaprnlem5N  42529  hdmaplkr  42542  hdmapip0  42544  hgmapvvlem2  42553  hgmapvvlem3  42554  hgmapvv  42555  redvmptabs  42974  readvrec2  42975  readvrec  42976  fiabv  43159  fsuppind  43177  0prjspnlem  43210  pellexlem5  43415  dfac11  43644  dfacbasgrp  43690  dgraalem  43727  dgraaub  43730  aaitgo  43744  proot1ex  43778  deg1mhm  43782  ofdivrec  44907  ofdivcan4  44908  ofdivdiv2  44909  expgrowth  44916  binomcxplemnotnn0  44937  dvdivbd  46502  dvdivcncf  46506  dirkeritg  46681  fourierdlem39  46725  fourierdlem57  46742  fourierdlem58  46743  fourierdlem59  46744  fourierdlem68  46753  fourierdlem76  46761  fourierdlem103  46788  fourierdlem104  46789  fourierdlem111  46796  setsnidel  47988  sprvalpwn0  48094  odz2prm2pw  48177  fmtnoprmfac1  48179  fmtnoprmfac2  48181  sfprmdvdsmersenne  48217  lighneallem2  48220  lighneallem3  48221  lighneal  48225  oddprmALTV  48314  evenprm2  48341  oddprmne2  48342  odd2prm2  48345  even3prm2  48346  isubgruhgr  48495  grimuhgr  48514  2zrngnmrid  48883  lincext1  49081  lindslinindsimp2lem5  49089  rege1logbrege0  49185  fllogbd  49187  relogbmulbexp  49188  relogbdivb  49189  nnpw2blen  49207  blennngt2o2  49219  blennn0e2  49221  dignn0ldlem  49229  line  49359  rrxline  49361  aacllem  50427