Theorem eldifsn 4719

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398   ∈ wcel 2114   ≠ wne 3016   ∖ cdif 3933  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-v 3496  df-dif 3939  df-sn 4568

This theorem is referenced by:  elpwdifsn  4721  eldifsni  4722  rexdifsn  4727  raldifsni  4728  eldifvsn  4730  difsn  4731  prproe  4836  sossfld  6043  tpres  6963  onmindif2  7527  mptsuppd  7853  suppssr  7861  suppssov1  7862  suppsssn  7865  suppssfv  7866  dif1o  8125  difsnen  8599  limenpsi  8692  frfi  8763  fofinf1o  8799  en2eleq  9434  en2other2  9435  dfac8clem  9458  acni2  9472  acndom  9477  acnnum  9478  dfac9  9562  dfacacn  9567  kmlem3  9578  kmlem4  9579  fin23lem21  9761  canthp1lem2  10075  elni  10298  mulnzcnopr  11286  divval  11300  elnnne0  11912  elq  12351  rpcndif0  12409  modfzo0difsn  13312  modsumfzodifsn  13313  expcl2lem  13442  expclzlem  13454  hashdifpr  13777  hashgt23el  13786  prprrab  13832  hashle2prv  13837  reccn2  14953  rlimdiv  15002  eff2  15452  tanval  15481  rpnnen2lem9  15575  fzo0dvdseq  15673  oddprmgt2  16043  oddprmdvds  16239  4sqlem19  16299  prmlem0  16439  prmlem1a  16440  setsnid  16539  grpinvnzcl  18171  symgextf  18545  f1omvdmvd  18571  pmtrprfv  18581  odcau  18729  efgsf  18855  efgsrel  18860  efgs1  18861  efgs1b  18862  efgsp1  18863  efgsres  18864  efgredlema  18866  efgredlemd  18870  efgrelexlemb  18876  gsumpt  19082  dmdprdd  19121  dprdcntz  19130  dprdfeq0  19144  dprd2da  19164  drngunit  19507  isdrng2  19512  drngid2  19518  isdrngd  19527  issubdrg  19560  sdrgacs  19580  cntzsdrg  19581  abvtriv  19612  islss  19706  lssneln0  19724  lssssr  19725  lbsind  19852  lbspss  19854  lspabs3  19893  lspsneq  19894  lspfixed  19900  lspexch  19901  islbs2  19926  isdomn2  20072  domnrrg  20073  mvrcl  20229  coe1tmmul2  20444  cnflddiv  20575  cnfldinv  20576  xrs1mnd  20583  xrs10  20584  xrge0subm  20586  cnsubdrglem  20596  cnmgpid  20607  cnmsubglem  20608  gzrngunit  20611  zringunit  20635  zringndrg  20637  domnchr  20679  cnmsgngrp  20723  psgninv  20726  psgndiflemB  20744  lindfind  20960  lindsind  20961  lindff1  20964  lindfrn  20965  mdetunilem9  21229  maducoeval2  21249  gsummatr01lem4  21267  ist1-2  21955  cmpfi  22016  2ndcdisj  22064  2ndcsep  22067  locfincmp  22134  alexsublem  22652  cldsubg  22719  imasdsf1olem  22983  prdsxmslem2  23139  reperflem  23426  xrge0gsumle  23441  xrge0tsms  23442  divcn  23476  evth  23563  cvsdiv  23736  cvsdivcl  23737  cphreccllem  23782  bcthlem5  23931  itg11  24292  i1fmullem  24295  i1fadd  24296  itg1addlem2  24298  i1fmulc  24304  itg1mulc  24305  ellimc3  24477  limcmpt2  24482  dvlem  24494  dvidlem  24513  dvcnp  24516  dvcobr  24543  dvrec  24552  dvrecg  24570  dvmptdiv  24571  dvcnvlem  24573  dvexp3  24575  dveflem  24576  dvferm1lem  24581  dvferm2lem  24583  lhop1lem  24610  ftc1lem5  24637  mdegleb  24658  coe1mul3  24693  ply1nz  24715  fta1blem  24762  fta1b  24763  ig1peu  24765  ig1pdvds  24770  plyeq0lem  24800  dgrub  24824  quotval  24881  fta1lem  24896  fta1  24897  elqaalem3  24910  qaa  24912  iaa  24914  aareccl  24915  aannenlem2  24918  abelthlem8  25027  abelth  25029  eff1olem  25132  logrncl  25151  eflog  25160  logeftb  25167  logdmss  25225  dvlog  25234  logbcl  25345  logbid1  25346  logb1  25347  elogb  25348  logbchbase  25349  relogbval  25350  relogbcl  25351  relogbreexp  25353  relogbmul  25355  nnlogbexp  25359  relogbcxp  25363  cxplogb  25364  relogbcxpb  25365  logbf  25367  logblog  25370  2logb9irrALT  25376  sqrt2cxp2logb9e3  25377  angval  25379  dcubic  25424  rlimcnp  25543  efrlim  25547  logexprlim  25801  dchrghm  25832  dchrabs  25836  lgsfcl2  25879  lgsval2lem  25883  lgsval3  25891  lgsmod  25899  lgsdirprm  25907  lgsne0  25911  gausslemma2dlem0f  25937  lgsquad2lem2  25961  2lgsoddprm  25992  2sqlem11  26005  2sqblem  26007  dchrvmaeq0  26080  rpvmasum2  26088  dchrisum0re  26089  qrngdiv  26200  tglngval  26337  tgisline  26413  axlowdimlem9  26736  axlowdimlem12  26739  axlowdimlem13  26740  elntg2  26771  upgrbi  26878  upgr1elem  26897  umgrislfupgrlem  26907  edgupgr  26919  subgruhgredgd  27066  upgrreslem  27086  nbgrel  27122  nbupgr  27126  nbupgrel  27127  nbumgrvtx  27128  nbgrssovtx  27143  nbupgrres  27146  nbusgrvtxm1uvtx  27187  nbupgruvtxres  27189  iscplgredg  27199  cusgredg  27206  cusgrfilem2  27238  usgredgsscusgredg  27241  1loopgrnb0  27284  1egrvtxdg0  27293  uhgrvd00  27316  vtxdginducedm1lem4  27324  eupth2lem3lem3  28009  frcond1  28045  frcond4  28049  2pthfrgr  28063  3cyclfrgrrn1  28064  n4cyclfrgr  28070  frgrwopreglem4a  28089  numclwwlk5  28167  suppss3  30460  xdivval  30595  xrge0tsmsd  30692  pmtrcnel  30733  pmtrcnelor  30735  0nellinds  30935  extdg1id  31053  submatminr1  31075  ordtconnlem1  31167  ispisys2  31412  sigapisys  31414  sibfinima  31597  sseqf  31650  signswch  31831  signstfvn  31839  signsvtn0  31840  signstfvneq0  31842  signstfvcl  31843  signstfveq0a  31846  signstfveq0  31847  signsvfn  31852  signsvtp  31853  signsvtn  31854  signsvfpn  31855  signsvfnn  31856  signlem0  31857  bnj158  31999  bnj168  32000  bnj529  32012  bnj906  32202  bnj970  32219  exdifsn  32345  cusgredgex2  32369  subfacp1lem5  32431  cvmsi  32512  cvmsval  32513  cvmsdisj  32517  cvmscld  32520  cvmsss2  32521  satfv1lem  32609  sinccvglem  32915  circum  32917  unbdqndv2lem2  33849  bj-0int  34396  lindsadd  34900  lindsenlbs  34902  matunitlindflem2  34904  matunitlindf  34905  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem16  34923  poimirlem18  34925  poimirlem19  34926  poimirlem21  34928  poimirlem22  34929  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  itg2addnclem2  34959  sdclem1  35033  rrncmslem  35125  rrnequiv  35128  isdrngo2  35251  isdrngo3  35252  prtlem100  36010  prter2  36032  prter3  36033  lsatlspsn2  36143  lsateln0  36146  lsatn0  36150  lsatspn0  36151  lsatcmp  36154  lsatelbN  36157  islshpat  36168  lsat0cv  36184  lkrlspeqN  36322  dvheveccl  38263  dihlatat  38488  dochnel  38544  dihjat1  38580  dvh4dimlem  38594  dochsnkr2cl  38625  dochkr1  38629  dochkr1OLDN  38630  lcfl6lem  38649  lcfl9a  38656  lclkrlem2l  38669  lclkrlem2o  38672  lclkrlem2q  38674  lcfrlem9  38701  lcfrlem16  38709  lcfrlem17  38710  lcfrlem27  38720  lcfrlem37  38730  lcfrlem38  38731  lcfrlem40  38733  lcdlkreqN  38773  mapdrvallem2  38796  mapdn0  38820  mapdpglem20  38842  mapdpglem30  38853  mapdindp0  38870  mapdhcl  38878  mapdh6aN  38886  mapdh6dN  38890  mapdh6eN  38891  mapdh6kN  38897  mapdh8  38939  hdmap1l6a  38960  hdmap1l6d  38964  hdmap1l6e  38965  hdmap1l6k  38971  hdmapval3N  38989  hdmap10  38991  hdmap11lem2  38993  hdmapnzcl  38996  hdmaprnlem3eN  39009  hdmaprnlem17N  39014  hdmap14lem4a  39022  hdmap14lem7  39025  hdmap14lem14  39032  hgmaprnlem5N  39051  hdmaplkr  39064  hdmapip0  39066  hgmapvvlem2  39075  hgmapvvlem3  39076  hgmapvv  39077  0prjspnlem  39288  pellexlem5  39450  dfac11  39682  dfacbasgrp  39728  dgraalem  39765  dgraaub  39768  aaitgo  39782  proot1ex  39821  isdomn3  39824  deg1mhm  39827  ofdivrec  40678  ofdivcan4  40679  ofdivdiv2  40680  expgrowth  40687  binomcxplemnotnn0  40708  dvdivbd  42228  dvdivcncf  42232  dirkeritg  42407  fourierdlem39  42451  fourierdlem57  42468  fourierdlem58  42469  fourierdlem59  42470  fourierdlem68  42479  fourierdlem76  42487  fourierdlem103  42514  fourierdlem104  42515  fourierdlem111  42522  setsnidel  43557  sprvalpwn0  43665  odz2prm2pw  43745  fmtnoprmfac1  43747  fmtnoprmfac2  43749  sfprmdvdsmersenne  43788  lighneallem2  43791  lighneallem3  43792  lighneal  43796  oddprmALTV  43872  evenprm2  43899  oddprmne2  43900  odd2prm2  43903  even3prm2  43904  2zrngnmrid  44241  lincext1  44529  lindslinindsimp2lem5  44537  rege1logbrege0  44638  fllogbd  44640  relogbmulbexp  44641  relogbdivb  44642  nnpw2blen  44660  blennngt2o2  44672  blennn0e2  44674  dignn0ldlem  44682  line  44739  rrxline  44741  aacllem  44922