Theorem eldifsn 4737

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 3913	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4591	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2962	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 574	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 275	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   ≠ wne 2925   ∖ cdif 3900  {csn 4577

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3438  df-dif 3906  df-sn 4578

This theorem is referenced by:  eldifsnd  4738  elpwdifsn  4740  eldifsni  4741  rexdifsn  4745  raldifsni  4746  eldifvsn  4748  difsn  4749  sossfld  6135  tpres  7137  onmindif2  7743  xpord3pred  8085  xpord3inddlem  8087  mptsuppd  8120  suppssr  8128  suppssov1  8130  suppssov2  8131  suppsssn  8134  suppssfv  8135  dif1o  8418  difsnen  8976  limenpsi  9069  frfi  9174  fofinf1o  9222  en2eleq  9902  en2other2  9903  dfac8clem  9926  acni2  9940  acndom  9945  acnnum  9946  dfac9  10031  dfacacn  10036  kmlem3  10047  kmlem4  10048  fin23lem21  10233  canthp1lem2  10547  elni  10770  mulnzcnf  11766  divval  11781  elnnne0  12398  elq  12851  rpcndif0  12914  modfzo0difsn  13850  modsumfzodifsn  13851  expcl2lem  13980  expclzlem  13990  hashdifpr  14322  hashgt23el  14331  prprrab  14380  hashle2prv  14385  reccn2  15504  rlimdiv  15553  eff2  16008  tanval  16037  rpnnen2lem9  16131  fzo0dvdseq  16234  oddprmgt2  16610  oddprmdvds  16815  4sqlem19  16875  prmlem0  17017  prmlem1a  17018  setsnid  17119  grpinvnzcl  18890  symgextf  19296  f1omvdmvd  19322  pmtrprfv  19332  odcau  19483  efgsf  19608  efgsrel  19613  efgs1  19614  efgs1b  19615  efgsp1  19616  efgsres  19617  efgredlema  19619  efgredlemd  19623  efgrelexlemb  19629  gsumpt  19841  dmdprdd  19880  dprdcntz  19889  dprdfeq0  19903  dprd2da  19923  isdomn2OLD  20597  domnrrg  20598  isdomn3  20600  drngunit  20619  isdrng2  20628  drngmcl  20635  drngid2  20637  isdrngd  20650  isdrngdOLD  20652  issubdrg  20665  sdrgacs  20686  cntzsdrg  20687  islss  20837  lssneln0  20856  lssssr  20857  lbsind  20984  lbspss  20986  lspabs3  21028  lspsneq  21029  lspfixed  21035  lspexch  21036  islbs2  21061  cnflddivOLD  21308  cnfldinv  21309  cnsubdrglem  21325  cnmgpid  21336  cnmsubglem  21337  gzrngunit  21340  xrs1mnd  21347  xrs10  21348  xrge0subm  21350  zringunit  21373  zringndrg  21375  domnchr  21439  cnmsgngrp  21486  psgninv  21489  psgndiflemB  21507  lindfind  21723  lindsind  21724  lindff1  21727  lindfrn  21728  mvrcl  21899  coe1tmmul2  22160  mdetunilem9  22505  maducoeval2  22525  gsummatr01lem4  22543  ist1-2  23232  cmpfi  23293  2ndcdisj  23341  2ndcsep  23344  locfincmp  23411  alexsublem  23929  cldsubg  23996  imasdsf1olem  24259  prdsxmslem2  24415  reperflem  24705  xrge0gsumle  24720  xrge0tsms  24721  divcnOLD  24755  divcn  24757  evth  24856  cvsdiv  25030  cvsdivcl  25031  cphreccllem  25076  bcthlem5  25226  itg11  25590  i1fmullem  25593  i1fadd  25594  itg1addlem2  25596  i1fmulc  25602  itg1mulc  25603  ellimc3  25778  limcmpt2  25783  dvlem  25795  dvidlem  25814  dvcnp  25818  dvcobr  25847  dvcobrOLD  25848  dvrec  25857  dvrecg  25875  dvmptdiv  25876  dvcnvlem  25878  dvexp3  25880  dveflem  25881  dvferm1lem  25886  dvferm2lem  25888  lhop1lem  25916  ftc1lem5  25945  mdegleb  25967  coe1mul3  26002  ply1nz  26025  fta1blem  26074  fta1b  26075  ig1peu  26078  ig1pdvds  26083  plyeq0lem  26113  dgrub  26137  quotval  26198  fta1lem  26213  fta1  26214  elqaalem3  26227  qaa  26229  iaa  26231  aareccl  26232  aannenlem2  26235  abelthlem8  26347  abelth  26349  eff1olem  26455  logrncl  26474  eflog  26483  logeftb  26490  logdmss  26549  dvlog  26558  logbcl  26675  logbid1  26676  logb1  26677  elogb  26678  logbchbase  26679  relogbval  26680  relogbcl  26681  relogbreexp  26683  relogbmul  26685  nnlogbexp  26689  relogbcxp  26693  cxplogb  26694  relogbcxpb  26695  logbf  26697  logblog  26700  2logb9irrALT  26706  sqrt2cxp2logb9e3  26707  angval  26709  dcubic  26754  rlimcnp  26873  efrlim  26877  efrlimOLD  26878  logexprlim  27134  dchrghm  27165  dchrabs  27169  lgsfcl2  27212  lgsval2lem  27216  lgsval3  27224  lgsmod  27232  lgsdirprm  27240  lgsne0  27244  gausslemma2dlem0f  27270  lgsquad2lem2  27294  2lgsoddprm  27325  2sqlem11  27338  2sqblem  27340  dchrvmaeq0  27413  rpvmasum2  27421  dchrisum0re  27422  qrngdiv  27533  addsval  27876  divsval  28099  elnns  28239  1nns  28248  tglngval  28500  tgisline  28576  axlowdimlem9  28899  axlowdimlem12  28902  axlowdimlem13  28903  elntg2  28934  upgrbi  29042  upgr1elem  29061  umgrislfupgrlem  29071  edgupgr  29083  subgruhgredgd  29233  upgrreslem  29253  nbgrel  29289  nbupgr  29293  nbupgrel  29294  nbumgrvtx  29295  nbgrssovtx  29310  nbupgrres  29313  nbusgrvtxm1uvtx  29354  nbupgruvtxres  29356  iscplgredg  29366  cusgredg  29373  cusgrfilem2  29406  usgredgsscusgredg  29409  1loopgrnb0  29452  1egrvtxdg0  29461  uhgrvd00  29484  vtxdginducedm1lem4  29492  eupth2lem3lem3  30178  frcond1  30214  frcond4  30218  2pthfrgr  30232  3cyclfrgrrn1  30233  n4cyclfrgr  30239  frgrwopreglem4a  30258  numclwwlk5  30336  ressupprn  32640  suppss3  32675  xdivval  32868  xrge0tsmsd  33024  pmtrcnel  33040  pmtrcnelor  33042  0nellinds  33316  dvdsruasso  33331  mxidlirredi  33417  extdg1id  33649  irngnzply1  33674  submatminr1  33793  ordtconnlem1  33907  ispisys2  34136  sigapisys  34138  sibfinima  34323  sseqf  34376  signswch  34545  signstfvn  34553  signsvtn0  34554  signstfvneq0  34556  signstfvcl  34557  signstfveq0a  34560  signstfveq0  34561  signsvfn  34566  signsvtp  34567  signsvtn  34568  signsvfpn  34569  signsvfnn  34570  signlem0  34571  bnj158  34712  bnj168  34713  bnj529  34724  bnj906  34913  bnj970  34930  exdifsn  35062  cusgredgex2  35116  subfacp1lem5  35177  cvmsi  35258  cvmsval  35259  cvmsdisj  35263  cvmscld  35266  cvmsss2  35267  satfv1lem  35355  sinccvglem  35665  circum  35667  mpomulnzcnf  36293  unbdqndv2lem2  36504  bj-0int  37095  lindsadd  37613  lindsenlbs  37615  matunitlindflem2  37617  matunitlindf  37618  poimirlem6  37626  poimirlem7  37627  poimirlem8  37628  poimirlem16  37636  poimirlem18  37638  poimirlem19  37639  poimirlem21  37641  poimirlem22  37642  poimirlem24  37644  poimirlem25  37645  poimirlem26  37646  poimirlem27  37647  itg2addnclem2  37672  sdclem1  37743  rrncmslem  37832  rrnequiv  37835  isdrngo2  37958  isdrngo3  37959  eldmxrncnvepres  38402  eldmxrncnvepres2  38403  prtlem100  38858  prter2  38880  prter3  38881  lsatlspsn2  38991  lsateln0  38994  lsatn0  38998  lsatspn0  38999  lsatcmp  39002  lsatelbN  39005  islshpat  39016  lsat0cv  39032  lkrlspeqN  39170  dvheveccl  41111  dihlatat  41336  dochnel  41392  dihjat1  41428  dvh4dimlem  41442  dochsnkr2cl  41473  dochkr1  41477  dochkr1OLDN  41478  lcfl6lem  41497  lcfl9a  41504  lclkrlem2l  41517  lclkrlem2o  41520  lclkrlem2q  41522  lcfrlem9  41549  lcfrlem16  41557  lcfrlem17  41558  lcfrlem27  41568  lcfrlem37  41578  lcfrlem38  41579  lcfrlem40  41581  lcdlkreqN  41621  mapdrvallem2  41644  mapdn0  41668  mapdpglem20  41690  mapdpglem30  41701  mapdindp0  41718  mapdhcl  41726  mapdh6aN  41734  mapdh6dN  41738  mapdh6eN  41739  mapdh6kN  41745  mapdh8  41787  hdmap1l6a  41808  hdmap1l6d  41812  hdmap1l6e  41813  hdmap1l6k  41819  hdmapval3N  41837  hdmap10  41839  hdmap11lem2  41841  hdmapnzcl  41844  hdmaprnlem3eN  41857  hdmaprnlem17N  41862  hdmap14lem4a  41870  hdmap14lem7  41873  hdmap14lem14  41880  hgmaprnlem5N  41899  hdmaplkr  41912  hdmapip0  41914  hgmapvvlem2  41923  hgmapvvlem3  41924  hgmapvv  41925  redvmptabs  42353  readvrec2  42354  readvrec  42355  fiabv  42529  fsuppind  42583  0prjspnlem  42616  pellexlem5  42826  dfac11  43055  dfacbasgrp  43101  dgraalem  43138  dgraaub  43141  aaitgo  43155  proot1ex  43189  deg1mhm  43193  ofdivrec  44319  ofdivcan4  44320  ofdivdiv2  44321  expgrowth  44328  binomcxplemnotnn0  44349  dvdivbd  45924  dvdivcncf  45928  dirkeritg  46103  fourierdlem39  46147  fourierdlem57  46164  fourierdlem58  46165  fourierdlem59  46166  fourierdlem68  46175  fourierdlem76  46183  fourierdlem103  46210  fourierdlem104  46211  fourierdlem111  46218  setsnidel  47381  sprvalpwn0  47487  odz2prm2pw  47567  fmtnoprmfac1  47569  fmtnoprmfac2  47571  sfprmdvdsmersenne  47607  lighneallem2  47610  lighneallem3  47611  lighneal  47615  oddprmALTV  47691  evenprm2  47718  oddprmne2  47719  odd2prm2  47722  even3prm2  47723  isubgruhgr  47872  grimuhgr  47891  2zrngnmrid  48260  lincext1  48459  lindslinindsimp2lem5  48467  rege1logbrege0  48563  fllogbd  48565  relogbmulbexp  48566  relogbdivb  48567  nnpw2blen  48585  blennngt2o2  48597  blennn0e2  48599  dignn0ldlem  48607  line  48737  rrxline  48739  aacllem  49806