Theorem eldifsn 4789

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 394   ∈ wcel 2104   ≠ wne 2938   ∖ cdif 3944  {csn 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-v 3474  df-dif 3950  df-sn 4628

This theorem is referenced by:  elpwdifsn  4791  eldifsni  4792  rexdifsn  4796  raldifsni  4797  eldifvsn  4799  difsn  4800  prproe  4905  sossfld  6184  tpres  7203  onmindif2  7797  xpord3pred  8140  xpord3inddlem  8142  mptsuppd  8174  suppssr  8183  suppssov1  8185  suppsssn  8188  suppssfv  8189  dif1o  8502  difsnen  9055  limenpsi  9154  frfi  9290  fofinf1o  9329  en2eleq  10005  en2other2  10006  dfac8clem  10029  acni2  10043  acndom  10048  acnnum  10049  dfac9  10133  dfacacn  10138  kmlem3  10149  kmlem4  10150  fin23lem21  10336  canthp1lem2  10650  elni  10873  mulnzcnopr  11864  divval  11878  elnnne0  12490  elq  12938  rpcndif0  12997  modfzo0difsn  13912  modsumfzodifsn  13913  expcl2lem  14043  expclzlem  14053  hashdifpr  14379  hashgt23el  14388  prprrab  14438  hashle2prv  14443  reccn2  15545  rlimdiv  15596  eff2  16046  tanval  16075  rpnnen2lem9  16169  fzo0dvdseq  16270  oddprmgt2  16640  oddprmdvds  16840  4sqlem19  16900  prmlem0  17043  prmlem1a  17044  setsnid  17146  setsnidOLD  17147  grpinvnzcl  18931  symgextf  19326  f1omvdmvd  19352  pmtrprfv  19362  odcau  19513  efgsf  19638  efgsrel  19643  efgs1  19644  efgs1b  19645  efgsp1  19646  efgsres  19647  efgredlema  19649  efgredlemd  19653  efgrelexlemb  19659  gsumpt  19871  dmdprdd  19910  dprdcntz  19919  dprdfeq0  19933  dprd2da  19953  drngunit  20505  isdrng2  20514  drngid2  20521  isdrngd  20533  isdrngdOLD  20535  issubdrg  20544  sdrgacs  20560  cntzsdrg  20561  abvtriv  20592  islss  20689  lssneln0  20707  lssssr  20708  lbsind  20835  lbspss  20837  lspabs3  20879  lspsneq  20880  lspfixed  20886  lspexch  20887  islbs2  20912  isdomn2  21115  domnrrg  21116  cnflddiv  21175  cnfldinv  21176  xrs1mnd  21183  xrs10  21184  xrge0subm  21186  cnsubdrglem  21196  cnmgpid  21207  cnmsubglem  21208  gzrngunit  21211  zringunit  21237  zringndrg  21239  domnchr  21303  cnmsgngrp  21351  psgninv  21354  psgndiflemB  21372  lindfind  21590  lindsind  21591  lindff1  21594  lindfrn  21595  mvrcl  21770  coe1tmmul2  22018  mdetunilem9  22342  maducoeval2  22362  gsummatr01lem4  22380  ist1-2  23071  cmpfi  23132  2ndcdisj  23180  2ndcsep  23183  locfincmp  23250  alexsublem  23768  cldsubg  23835  imasdsf1olem  24099  prdsxmslem2  24258  reperflem  24554  xrge0gsumle  24569  xrge0tsms  24570  divcnOLD  24604  divcn  24606  evth  24705  cvsdiv  24879  cvsdivcl  24880  cphreccllem  24926  bcthlem5  25076  itg11  25440  i1fmullem  25443  i1fadd  25444  itg1addlem2  25446  i1fmulc  25453  itg1mulc  25454  ellimc3  25628  limcmpt2  25633  dvlem  25645  dvidlem  25664  dvcnp  25668  dvcobr  25697  dvcobrOLD  25698  dvrec  25707  dvrecg  25725  dvmptdiv  25726  dvcnvlem  25728  dvexp3  25730  dveflem  25731  dvferm1lem  25736  dvferm2lem  25738  lhop1lem  25765  ftc1lem5  25792  mdegleb  25817  coe1mul3  25852  ply1nz  25874  fta1blem  25921  fta1b  25922  ig1peu  25924  ig1pdvds  25929  plyeq0lem  25959  dgrub  25983  quotval  26041  fta1lem  26056  fta1  26057  elqaalem3  26070  qaa  26072  iaa  26074  aareccl  26075  aannenlem2  26078  abelthlem8  26187  abelth  26189  eff1olem  26293  logrncl  26312  eflog  26321  logeftb  26328  logdmss  26386  dvlog  26395  logbcl  26508  logbid1  26509  logb1  26510  elogb  26511  logbchbase  26512  relogbval  26513  relogbcl  26514  relogbreexp  26516  relogbmul  26518  nnlogbexp  26522  relogbcxp  26526  cxplogb  26527  relogbcxpb  26528  logbf  26530  logblog  26533  2logb9irrALT  26539  sqrt2cxp2logb9e3  26540  angval  26542  dcubic  26587  rlimcnp  26706  efrlim  26710  logexprlim  26964  dchrghm  26995  dchrabs  26999  lgsfcl2  27042  lgsval2lem  27046  lgsval3  27054  lgsmod  27062  lgsdirprm  27070  lgsne0  27074  gausslemma2dlem0f  27100  lgsquad2lem2  27124  2lgsoddprm  27155  2sqlem11  27168  2sqblem  27170  dchrvmaeq0  27243  rpvmasum2  27251  dchrisum0re  27252  qrngdiv  27363  addsval  27684  divsval  27876  tglngval  28069  tgisline  28145  axlowdimlem9  28475  axlowdimlem12  28478  axlowdimlem13  28479  elntg2  28510  upgrbi  28620  upgr1elem  28639  umgrislfupgrlem  28649  edgupgr  28661  subgruhgredgd  28808  upgrreslem  28828  nbgrel  28864  nbupgr  28868  nbupgrel  28869  nbumgrvtx  28870  nbgrssovtx  28885  nbupgrres  28888  nbusgrvtxm1uvtx  28929  nbupgruvtxres  28931  iscplgredg  28941  cusgredg  28948  cusgrfilem2  28980  usgredgsscusgredg  28983  1loopgrnb0  29026  1egrvtxdg0  29035  uhgrvd00  29058  vtxdginducedm1lem4  29066  eupth2lem3lem3  29750  frcond1  29786  frcond4  29790  2pthfrgr  29804  3cyclfrgrrn1  29805  n4cyclfrgr  29811  frgrwopreglem4a  29830  numclwwlk5  29908  ressupprn  32179  suppss3  32216  xdivval  32352  xrge0tsmsd  32479  pmtrcnel  32520  pmtrcnelor  32522  0nellinds  32757  dvdsruasso  32764  mxidlirredi  32861  extdg1id  33030  irngnzply1  33044  submatminr1  33088  ordtconnlem1  33202  ispisys2  33449  sigapisys  33451  sibfinima  33636  sseqf  33689  signswch  33870  signstfvn  33878  signsvtn0  33879  signstfvneq0  33881  signstfvcl  33882  signstfveq0a  33885  signstfveq0  33886  signsvfn  33891  signsvtp  33892  signsvtn  33893  signsvfpn  33894  signsvfnn  33895  signlem0  33896  bnj158  34038  bnj168  34039  bnj529  34050  bnj906  34239  bnj970  34256  exdifsn  34382  cusgredgex2  34411  subfacp1lem5  34473  cvmsi  34554  cvmsval  34555  cvmsdisj  34559  cvmscld  34562  cvmsss2  34563  satfv1lem  34651  sinccvglem  34955  circum  34957  unbdqndv2lem2  35689  bj-0int  36285  lindsadd  36784  lindsenlbs  36786  matunitlindflem2  36788  matunitlindf  36789  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem16  36807  poimirlem18  36809  poimirlem19  36810  poimirlem21  36812  poimirlem22  36813  poimirlem24  36815  poimirlem25  36816  poimirlem26  36817  poimirlem27  36818  itg2addnclem2  36843  sdclem1  36914  rrncmslem  37003  rrnequiv  37006  isdrngo2  37129  isdrngo3  37130  prtlem100  38032  prter2  38054  prter3  38055  lsatlspsn2  38165  lsateln0  38168  lsatn0  38172  lsatspn0  38173  lsatcmp  38176  lsatelbN  38179  islshpat  38190  lsat0cv  38206  lkrlspeqN  38344  dvheveccl  40286  dihlatat  40511  dochnel  40567  dihjat1  40603  dvh4dimlem  40617  dochsnkr2cl  40648  dochkr1  40652  dochkr1OLDN  40653  lcfl6lem  40672  lcfl9a  40679  lclkrlem2l  40692  lclkrlem2o  40695  lclkrlem2q  40697  lcfrlem9  40724  lcfrlem16  40732  lcfrlem17  40733  lcfrlem27  40743  lcfrlem37  40753  lcfrlem38  40754  lcfrlem40  40756  lcdlkreqN  40796  mapdrvallem2  40819  mapdn0  40843  mapdpglem20  40865  mapdpglem30  40876  mapdindp0  40893  mapdhcl  40901  mapdh6aN  40909  mapdh6dN  40913  mapdh6eN  40914  mapdh6kN  40920  mapdh8  40962  hdmap1l6a  40983  hdmap1l6d  40987  hdmap1l6e  40988  hdmap1l6k  40994  hdmapval3N  41012  hdmap10  41014  hdmap11lem2  41016  hdmapnzcl  41019  hdmaprnlem3eN  41032  hdmaprnlem17N  41037  hdmap14lem4a  41045  hdmap14lem7  41048  hdmap14lem14  41055  hgmaprnlem5N  41074  hdmaplkr  41087  hdmapip0  41089  hgmapvvlem2  41098  hgmapvvlem3  41099  hgmapvv  41100  fsuppind  41464  0prjspnlem  41667  pellexlem5  41873  dfac11  42106  dfacbasgrp  42152  dgraalem  42189  dgraaub  42192  aaitgo  42206  proot1ex  42245  isdomn3  42248  deg1mhm  42251  ofdivrec  43387  ofdivcan4  43388  ofdivdiv2  43389  expgrowth  43396  binomcxplemnotnn0  43417  dvdivbd  44937  dvdivcncf  44941  dirkeritg  45116  fourierdlem39  45160  fourierdlem57  45177  fourierdlem58  45178  fourierdlem59  45179  fourierdlem68  45188  fourierdlem76  45196  fourierdlem103  45223  fourierdlem104  45224  fourierdlem111  45231  setsnidel  46343  sprvalpwn0  46449  odz2prm2pw  46529  fmtnoprmfac1  46531  fmtnoprmfac2  46533  sfprmdvdsmersenne  46569  lighneallem2  46572  lighneallem3  46573  lighneal  46577  oddprmALTV  46653  evenprm2  46680  oddprmne2  46681  odd2prm2  46684  even3prm2  46685  2zrngnmrid  46936  lincext1  47222  lindslinindsimp2lem5  47230  rege1logbrege0  47331  fllogbd  47333  relogbmulbexp  47334  relogbdivb  47335  nnpw2blen  47353  blennngt2o2  47365  blennn0e2  47367  dignn0ldlem  47375  line  47505  rrxline  47507  aacllem  47935