Theorem eldifsn 4722

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 397   ∈ wcel 2121   ≠ wne 2936   ∖ cdif 3882  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-v 3435  df-dif 3888  df-sn 4559

This theorem is referenced by:  eldifsnd  4723  eldifsni  4726  rexdifsn  4730  raldifsni  4731  eldifvsn  4733  difsn  4734  sossfld  6141  tpres  7149  onmindif2  7754  xpord3pred  8096  xpord3inddlem  8098  mptsuppd  8131  suppssr  8139  suppssov1  8141  suppssov2  8142  suppsssn  8145  suppssfv  8146  dif1o  8429  difsnen  8991  limenpsi  9084  frfi  9189  fofinf1o  9236  en2eleq  9925  en2other2  9926  dfac8clem  9949  acni2  9963  acndom  9968  acnnum  9969  dfac9  10054  dfacacn  10059  kmlem3  10070  kmlem4  10071  fin23lem21  10256  canthp1lem2  10571  elni  10794  mulnzcnf  11791  divval  11806  elnnne0  12446  elq  12895  rpcndif0  12958  modfzo0difsn  13900  modsumfzodifsn  13901  expcl2lem  14030  expclzlem  14040  hashdifpr  14372  hashgt23el  14381  prprrab  14430  hashle2prv  14435  reccn2  15554  rlimdiv  15603  eff2  16061  tanval  16090  rpnnen2lem9  16184  fzo0dvdseq  16287  oddprmgt2  16664  oddprmdvds  16869  4sqlem19  16929  prmlem0  17071  prmlem1a  17072  setsnid  17173  grpinvnzcl  18982  symgextf  19387  f1omvdmvd  19413  pmtrprfv  19423  odcau  19574  efgsf  19699  efgsrel  19704  efgs1  19705  efgs1b  19706  efgsp1  19707  efgsres  19708  efgredlema  19710  efgredlemd  19714  efgrelexlemb  19720  gsumpt  19932  dmdprdd  19971  dprdcntz  19980  dprdfeq0  19994  dprd2da  20014  isdomn2OLD  20688  domnrrg  20689  isdomn3  20691  drngunit  20710  isdrng2  20719  drngmcl  20726  drngid2  20728  isdrngd  20741  isdrngdOLD  20743  issubdrg  20756  sdrgacs  20777  cntzsdrg  20778  islss  20928  lssneln0  20947  lssssr  20948  lbsind  21074  lbspss  21076  lspabs3  21118  lspsneq  21119  lspfixed  21125  lspexch  21126  islbs2  21151  cnfldinv  21382  cnsubdrglem  21397  cnmgpid  21408  cnmsubglem  21409  gzrngunit  21412  xrs1mnd  21419  xrs10  21420  xrge0subm  21422  zringunit  21445  zringndrg  21447  domnchr  21511  cnmsgngrp  21558  psgninv  21561  psgndiflemB  21579  lindfind  21795  lindsind  21796  lindff1  21799  lindfrn  21800  mvrcl  21970  coe1tmmul2  22266  mdetunilem9  22607  maducoeval2  22627  gsummatr01lem4  22645  ist1-2  23334  cmpfi  23395  2ndcdisj  23443  2ndcsep  23446  locfincmp  23513  alexsublem  24031  cldsubg  24098  imasdsf1olem  24360  prdsxmslem2  24516  reperflem  24806  xrge0gsumle  24821  xrge0tsms  24822  divcn  24857  evth  24948  cvsdiv  25121  cvsdivcl  25122  cphreccllem  25167  bcthlem5  25317  itg11  25680  i1fmullem  25683  i1fadd  25684  itg1addlem2  25686  i1fmulc  25692  itg1mulc  25693  ellimc3  25868  limcmpt2  25873  dvlem  25885  dvidlem  25904  dvcnp  25908  dvcobr  25935  dvrec  25944  dvrecg  25962  dvmptdiv  25963  dvcnvlem  25965  dvexp3  25967  dveflem  25968  dvferm1lem  25973  dvferm2lem  25975  lhop1lem  26002  ftc1lem5  26029  mdegleb  26051  coe1mul3  26086  ply1nz  26109  fta1blem  26158  fta1b  26159  ig1peu  26162  ig1pdvds  26167  plyeq0lem  26197  dgrub  26221  quotval  26280  fta1lem  26295  fta1  26296  elqaalem3  26309  qaa  26311  iaa  26313  aareccl  26314  aannenlem2  26317  abelthlem8  26426  abelth  26428  eff1olem  26534  logrncl  26553  eflog  26562  logeftb  26569  logdmss  26628  dvlog  26637  logbcl  26753  logbid1  26754  logb1  26755  elogb  26756  logbchbase  26757  relogbval  26758  relogbcl  26759  relogbreexp  26761  relogbmul  26763  nnlogbexp  26767  relogbcxp  26771  cxplogb  26772  relogbcxpb  26773  logbf  26775  logblog  26778  2logb9irrALT  26784  sqrt2cxp2logb9e3  26785  angval  26787  dcubic  26832  rlimcnp  26951  efrlim  26955  logexprlim  27210  dchrghm  27241  dchrabs  27245  lgsfcl2  27288  lgsval2lem  27292  lgsval3  27300  lgsmod  27308  lgsdirprm  27316  lgsne0  27320  gausslemma2dlem0f  27346  lgsquad2lem2  27370  2lgsoddprm  27401  2sqlem11  27414  2sqblem  27416  dchrvmaeq0  27489  rpvmasum2  27497  dchrisum0re  27498  qrngdiv  27609  addsval  27976  divsval  28203  elnns  28354  1nns  28363  tglngval  28641  tgisline  28717  axlowdimlem9  29041  axlowdimlem12  29044  axlowdimlem13  29045  elntg2  29076  upgrbi  29184  upgr1elem  29203  umgrislfupgrlem  29213  edgupgr  29225  subgruhgredgd  29375  upgrreslem  29395  nbgrel  29431  nbupgr  29435  nbupgrel  29436  nbumgrvtx  29437  nbgrssovtx  29452  nbupgrres  29455  nbusgrvtxm1uvtx  29496  nbupgruvtxres  29498  iscplgredg  29508  cusgredg  29515  cusgrfilem2  29547  usgredgsscusgredg  29550  1loopgrnb0  29593  1egrvtxdg0  29602  uhgrvd00  29625  vtxdginducedm1lem4  29633  eupth2lem3lem3  30322  frcond1  30358  frcond4  30362  2pthfrgr  30376  3cyclfrgrrn1  30377  n4cyclfrgr  30383  frgrwopreglem4a  30402  numclwwlk5  30480  ressupprn  32786  suppss3  32819  xdivval  33001  xrge0tsmsd  33158  pmtrcnel  33174  pmtrcnelor  33176  0nellinds  33457  dvdsruasso  33472  extdg1id  33862  irngnzply1  33887  submatminr1  34006  ordtconnlem1  34120  ispisys2  34349  sigapisys  34351  sibfinima  34535  sseqf  34588  signswch  34757  signstfvn  34765  signsvtn0  34766  signstfvneq0  34768  signstfvcl  34769  signstfveq0a  34772  signstfveq0  34773  signsvfn  34778  signsvtp  34779  signsvtn  34780  signsvfpn  34781  signsvfnn  34782  signlem0  34783  bnj158  34927  bnj168  34928  bnj529  34939  bnj906  35127  bnj970  35144  exdifsn  35276  cusgredgex2  35366  subfacp1lem5  35427  cvmsi  35508  cvmsval  35509  cvmsdisj  35513  cvmscld  35516  cvmsss2  35517  satfv1lem  35605  sinccvglem  35915  circum  35917  mpomulnzcnf  36542  unbdqndv2lem2  36831  bj-0int  37474  lindsadd  37995  lindsenlbs  37997  matunitlindflem2  37999  matunitlindf  38000  poimirlem6  38008  poimirlem7  38009  poimirlem8  38010  poimirlem16  38018  poimirlem18  38020  poimirlem19  38021  poimirlem21  38023  poimirlem22  38024  poimirlem24  38026  poimirlem25  38027  poimirlem26  38028  poimirlem27  38029  itg2addnclem2  38054  sdclem1  38125  rrncmslem  38214  rrnequiv  38217  isdrngo2  38340  isdrngo3  38341  eldmxrncnvepres  38816  eldmxrncnvepres2  38817  prtlem100  39366  prter2  39388  prter3  39389  lsatlspsn2  39499  lsateln0  39502  lsatn0  39506  lsatspn0  39507  lsatcmp  39510  lsatelbN  39513  islshpat  39524  lsat0cv  39540  lkrlspeqN  39678  dvheveccl  41619  dihlatat  41844  dochnel  41900  dihjat1  41936  dvh4dimlem  41950  dochsnkr2cl  41981  dochkr1  41985  dochkr1OLDN  41986  lcfl6lem  42005  lcfl9a  42012  lclkrlem2l  42025  lclkrlem2o  42028  lclkrlem2q  42030  lcfrlem9  42057  lcfrlem16  42065  lcfrlem17  42066  lcfrlem27  42076  lcfrlem37  42086  lcfrlem38  42087  lcfrlem40  42089  lcdlkreqN  42129  mapdrvallem2  42152  mapdn0  42176  mapdpglem20  42198  mapdpglem30  42209  mapdindp0  42226  mapdhcl  42234  mapdh6aN  42242  mapdh6dN  42246  mapdh6eN  42247  mapdh6kN  42253  mapdh8  42295  hdmap1l6a  42316  hdmap1l6d  42320  hdmap1l6e  42321  hdmap1l6k  42327  hdmapval3N  42345  hdmap10  42347  hdmap11lem2  42349  hdmapnzcl  42352  hdmaprnlem3eN  42365  hdmaprnlem17N  42370  hdmap14lem4a  42378  hdmap14lem7  42381  hdmap14lem14  42388  hgmaprnlem5N  42407  hdmaplkr  42420  hdmapip0  42422  hgmapvvlem2  42431  hgmapvvlem3  42432  hgmapvv  42433  redvmptabs  42852  readvrec2  42853  readvrec  42854  fiabv  43037  fsuppind  43055  0prjspnlem  43088  pellexlem5  43293  dfac11  43522  dfacbasgrp  43568  dgraalem  43605  dgraaub  43608  aaitgo  43622  proot1ex  43656  deg1mhm  43660  ofdivrec  44785  ofdivcan4  44786  ofdivdiv2  44787  expgrowth  44794  binomcxplemnotnn0  44815  dvdivbd  46380  dvdivcncf  46384  dirkeritg  46559  fourierdlem39  46603  fourierdlem57  46620  fourierdlem58  46621  fourierdlem59  46622  fourierdlem68  46631  fourierdlem76  46639  fourierdlem103  46666  fourierdlem104  46667  fourierdlem111  46674  setsnidel  47866  sprvalpwn0  47972  odz2prm2pw  48055  fmtnoprmfac1  48057  fmtnoprmfac2  48059  sfprmdvdsmersenne  48095  lighneallem2  48098  lighneallem3  48099  lighneal  48103  oddprmALTV  48192  evenprm2  48219  oddprmne2  48220  odd2prm2  48223  even3prm2  48224  isubgruhgr  48373  grimuhgr  48392  2zrngnmrid  48761  lincext1  48959  lindslinindsimp2lem5  48967  rege1logbrege0  49063  fllogbd  49065  relogbmulbexp  49066  relogbdivb  49067  nnpw2blen  49085  blennngt2o2  49097  blennn0e2  49099  dignn0ldlem  49107  line  49237  rrxline  49239  aacllem  50305