Theorem eldifsn 4741

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   ≠ wne 2931   ∖ cdif 3897  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ne 2932  df-v 3441  df-dif 3903  df-sn 4580

This theorem is referenced by:  eldifsnd  4742  elpwdifsn  4744  eldifsni  4745  rexdifsn  4749  raldifsni  4750  eldifvsn  4752  difsn  4753  sossfld  6143  tpres  7147  onmindif2  7752  xpord3pred  8094  xpord3inddlem  8096  mptsuppd  8129  suppssr  8137  suppssov1  8139  suppssov2  8140  suppsssn  8143  suppssfv  8144  dif1o  8427  difsnen  8989  limenpsi  9082  frfi  9187  fofinf1o  9234  en2eleq  9920  en2other2  9921  dfac8clem  9944  acni2  9958  acndom  9963  acnnum  9964  dfac9  10049  dfacacn  10054  kmlem3  10065  kmlem4  10066  fin23lem21  10251  canthp1lem2  10566  elni  10789  mulnzcnf  11785  divval  11800  elnnne0  12417  elq  12865  rpcndif0  12928  modfzo0difsn  13868  modsumfzodifsn  13869  expcl2lem  13998  expclzlem  14008  hashdifpr  14340  hashgt23el  14349  prprrab  14398  hashle2prv  14403  reccn2  15522  rlimdiv  15571  eff2  16026  tanval  16055  rpnnen2lem9  16149  fzo0dvdseq  16252  oddprmgt2  16628  oddprmdvds  16833  4sqlem19  16893  prmlem0  17035  prmlem1a  17036  setsnid  17137  grpinvnzcl  18943  symgextf  19348  f1omvdmvd  19374  pmtrprfv  19384  odcau  19535  efgsf  19660  efgsrel  19665  efgs1  19666  efgs1b  19667  efgsp1  19668  efgsres  19669  efgredlema  19671  efgredlemd  19675  efgrelexlemb  19681  gsumpt  19893  dmdprdd  19932  dprdcntz  19941  dprdfeq0  19955  dprd2da  19975  isdomn2OLD  20647  domnrrg  20648  isdomn3  20650  drngunit  20669  isdrng2  20678  drngmcl  20685  drngid2  20687  isdrngd  20700  isdrngdOLD  20702  issubdrg  20715  sdrgacs  20736  cntzsdrg  20737  islss  20887  lssneln0  20906  lssssr  20907  lbsind  21034  lbspss  21036  lspabs3  21078  lspsneq  21079  lspfixed  21085  lspexch  21086  islbs2  21111  cnflddivOLD  21358  cnfldinv  21359  cnsubdrglem  21375  cnmgpid  21386  cnmsubglem  21387  gzrngunit  21390  xrs1mnd  21397  xrs10  21398  xrge0subm  21400  zringunit  21423  zringndrg  21425  domnchr  21489  cnmsgngrp  21536  psgninv  21539  psgndiflemB  21557  lindfind  21773  lindsind  21774  lindff1  21777  lindfrn  21778  mvrcl  21949  coe1tmmul2  22220  mdetunilem9  22566  maducoeval2  22586  gsummatr01lem4  22604  ist1-2  23293  cmpfi  23354  2ndcdisj  23402  2ndcsep  23405  locfincmp  23472  alexsublem  23990  cldsubg  24057  imasdsf1olem  24319  prdsxmslem2  24475  reperflem  24765  xrge0gsumle  24780  xrge0tsms  24781  divcnOLD  24815  divcn  24817  evth  24916  cvsdiv  25090  cvsdivcl  25091  cphreccllem  25136  bcthlem5  25286  itg11  25650  i1fmullem  25653  i1fadd  25654  itg1addlem2  25656  i1fmulc  25662  itg1mulc  25663  ellimc3  25838  limcmpt2  25843  dvlem  25855  dvidlem  25874  dvcnp  25878  dvcobr  25907  dvcobrOLD  25908  dvrec  25917  dvrecg  25935  dvmptdiv  25936  dvcnvlem  25938  dvexp3  25940  dveflem  25941  dvferm1lem  25946  dvferm2lem  25948  lhop1lem  25976  ftc1lem5  26005  mdegleb  26027  coe1mul3  26062  ply1nz  26085  fta1blem  26134  fta1b  26135  ig1peu  26138  ig1pdvds  26143  plyeq0lem  26173  dgrub  26197  quotval  26258  fta1lem  26273  fta1  26274  elqaalem3  26287  qaa  26289  iaa  26291  aareccl  26292  aannenlem2  26295  abelthlem8  26407  abelth  26409  eff1olem  26515  logrncl  26534  eflog  26543  logeftb  26550  logdmss  26609  dvlog  26618  logbcl  26735  logbid1  26736  logb1  26737  elogb  26738  logbchbase  26739  relogbval  26740  relogbcl  26741  relogbreexp  26743  relogbmul  26745  nnlogbexp  26749  relogbcxp  26753  cxplogb  26754  relogbcxpb  26755  logbf  26757  logblog  26760  2logb9irrALT  26766  sqrt2cxp2logb9e3  26767  angval  26769  dcubic  26814  rlimcnp  26933  efrlim  26937  efrlimOLD  26938  logexprlim  27194  dchrghm  27225  dchrabs  27229  lgsfcl2  27272  lgsval2lem  27276  lgsval3  27284  lgsmod  27292  lgsdirprm  27300  lgsne0  27304  gausslemma2dlem0f  27330  lgsquad2lem2  27354  2lgsoddprm  27385  2sqlem11  27398  2sqblem  27400  dchrvmaeq0  27473  rpvmasum2  27481  dchrisum0re  27482  qrngdiv  27593  addsval  27942  divsval  28169  elnns  28318  1nns  28327  tglngval  28604  tgisline  28680  axlowdimlem9  29004  axlowdimlem12  29007  axlowdimlem13  29008  elntg2  29039  upgrbi  29147  upgr1elem  29166  umgrislfupgrlem  29176  edgupgr  29188  subgruhgredgd  29338  upgrreslem  29358  nbgrel  29394  nbupgr  29398  nbupgrel  29399  nbumgrvtx  29400  nbgrssovtx  29415  nbupgrres  29418  nbusgrvtxm1uvtx  29459  nbupgruvtxres  29461  iscplgredg  29471  cusgredg  29478  cusgrfilem2  29511  usgredgsscusgredg  29514  1loopgrnb0  29557  1egrvtxdg0  29566  uhgrvd00  29589  vtxdginducedm1lem4  29597  eupth2lem3lem3  30286  frcond1  30322  frcond4  30326  2pthfrgr  30340  3cyclfrgrrn1  30341  n4cyclfrgr  30347  frgrwopreglem4a  30366  numclwwlk5  30444  ressupprn  32748  suppss3  32781  xdivval  32979  xrge0tsmsd  33134  pmtrcnel  33150  pmtrcnelor  33152  0nellinds  33430  dvdsruasso  33445  mxidlirredi  33531  extdg1id  33802  irngnzply1  33827  submatminr1  33946  ordtconnlem1  34060  ispisys2  34289  sigapisys  34291  sibfinima  34475  sseqf  34528  signswch  34697  signstfvn  34705  signsvtn0  34706  signstfvneq0  34708  signstfvcl  34709  signstfveq0a  34712  signstfveq0  34713  signsvfn  34718  signsvtp  34719  signsvtn  34720  signsvfpn  34721  signsvfnn  34722  signlem0  34723  bnj158  34864  bnj168  34865  bnj529  34876  bnj906  35065  bnj970  35082  exdifsn  35214  cusgredgex2  35296  subfacp1lem5  35357  cvmsi  35438  cvmsval  35439  cvmsdisj  35443  cvmscld  35446  cvmsss2  35447  satfv1lem  35535  sinccvglem  35845  circum  35847  mpomulnzcnf  36472  unbdqndv2lem2  36683  bj-0int  37275  lindsadd  37783  lindsenlbs  37785  matunitlindflem2  37787  matunitlindf  37788  poimirlem6  37796  poimirlem7  37797  poimirlem8  37798  poimirlem16  37806  poimirlem18  37808  poimirlem19  37809  poimirlem21  37811  poimirlem22  37812  poimirlem24  37814  poimirlem25  37815  poimirlem26  37816  poimirlem27  37817  itg2addnclem2  37842  sdclem1  37913  rrncmslem  38002  rrnequiv  38005  isdrngo2  38128  isdrngo3  38129  eldmxrncnvepres  38604  eldmxrncnvepres2  38605  prtlem100  39154  prter2  39176  prter3  39177  lsatlspsn2  39287  lsateln0  39290  lsatn0  39294  lsatspn0  39295  lsatcmp  39298  lsatelbN  39301  islshpat  39312  lsat0cv  39328  lkrlspeqN  39466  dvheveccl  41407  dihlatat  41632  dochnel  41688  dihjat1  41724  dvh4dimlem  41738  dochsnkr2cl  41769  dochkr1  41773  dochkr1OLDN  41774  lcfl6lem  41793  lcfl9a  41800  lclkrlem2l  41813  lclkrlem2o  41816  lclkrlem2q  41818  lcfrlem9  41845  lcfrlem16  41853  lcfrlem17  41854  lcfrlem27  41864  lcfrlem37  41874  lcfrlem38  41875  lcfrlem40  41877  lcdlkreqN  41917  mapdrvallem2  41940  mapdn0  41964  mapdpglem20  41986  mapdpglem30  41997  mapdindp0  42014  mapdhcl  42022  mapdh6aN  42030  mapdh6dN  42034  mapdh6eN  42035  mapdh6kN  42041  mapdh8  42083  hdmap1l6a  42104  hdmap1l6d  42108  hdmap1l6e  42109  hdmap1l6k  42115  hdmapval3N  42133  hdmap10  42135  hdmap11lem2  42137  hdmapnzcl  42140  hdmaprnlem3eN  42153  hdmaprnlem17N  42158  hdmap14lem4a  42166  hdmap14lem7  42169  hdmap14lem14  42176  hgmaprnlem5N  42195  hdmaplkr  42208  hdmapip0  42210  hgmapvvlem2  42219  hgmapvvlem3  42220  hgmapvv  42221  redvmptabs  42652  readvrec2  42653  readvrec  42654  fiabv  42828  fsuppind  42870  0prjspnlem  42903  pellexlem5  43112  dfac11  43341  dfacbasgrp  43387  dgraalem  43424  dgraaub  43427  aaitgo  43441  proot1ex  43475  deg1mhm  43479  ofdivrec  44604  ofdivcan4  44605  ofdivdiv2  44606  expgrowth  44613  binomcxplemnotnn0  44634  dvdivbd  46204  dvdivcncf  46208  dirkeritg  46383  fourierdlem39  46427  fourierdlem57  46444  fourierdlem58  46445  fourierdlem59  46446  fourierdlem68  46455  fourierdlem76  46463  fourierdlem103  46490  fourierdlem104  46491  fourierdlem111  46498  setsnidel  47660  sprvalpwn0  47766  odz2prm2pw  47846  fmtnoprmfac1  47848  fmtnoprmfac2  47850  sfprmdvdsmersenne  47886  lighneallem2  47889  lighneallem3  47890  lighneal  47894  oddprmALTV  47970  evenprm2  47997  oddprmne2  47998  odd2prm2  48001  even3prm2  48002  isubgruhgr  48151  grimuhgr  48170  2zrngnmrid  48539  lincext1  48737  lindslinindsimp2lem5  48745  rege1logbrege0  48841  fllogbd  48843  relogbmulbexp  48844  relogbdivb  48845  nnpw2blen  48863  blennngt2o2  48875  blennn0e2  48877  dignn0ldlem  48885  line  49015  rrxline  49017  aacllem  50083