Theorem eldifsn 4628

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 3871	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4488	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 3020	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 575	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 276	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396   ∈ wcel 2080   ≠ wne 2983   ∖ cdif 3858  {csn 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-v 3438  df-dif 3864  df-sn 4475

This theorem is referenced by:  elpwdifsn  4630  eldifsni  4631  rexdifsn  4636  raldifsni  4637  eldifvsn  4639  difsn  4640  prproe  4745  sossfld  5922  tpres  6833  onmindif2  7386  mptsuppd  7707  suppssr  7715  suppssov1  7716  suppsssn  7719  suppssfv  7720  dif1o  7979  difsnen  8449  limenpsi  8542  frfi  8612  fofinf1o  8648  en2eleq  9283  en2other2  9284  dfac8clem  9307  acni2  9321  acndom  9326  acnnum  9327  dfac9  9411  dfacacn  9416  kmlem3  9427  kmlem4  9428  fin23lem21  9610  canthp1lem2  9924  elni  10147  mulnzcnopr  11136  divval  11150  elnnne0  11761  elq  12199  rpcndif0  12258  modfzo0difsn  13161  modsumfzodifsn  13162  expcl2lem  13291  expclzlem  13303  hashdifpr  13624  hashgt23el  13633  prprrab  13677  hashle2prv  13682  reccn2  14787  rlimdiv  14836  eff2  15285  tanval  15314  rpnnen2lem9  15408  fzo0dvdseq  15506  oddprmgt2  15872  oddprmdvds  16068  4sqlem19  16128  prmlem0  16268  prmlem1a  16269  setsnid  16368  grpinvnzcl  17928  symgextf  18276  f1omvdmvd  18302  pmtrprfv  18312  odcau  18459  efgsf  18582  efgsrel  18587  efgs1  18588  efgs1b  18589  efgsp1  18590  efgsres  18591  efgredlema  18593  efgredlemd  18597  efgrelexlemb  18603  gsumpt  18802  dmdprdd  18838  dprdcntz  18847  dprdfeq0  18861  dprd2da  18881  drngunit  19197  isdrng2  19202  drngid2  19208  isdrngd  19217  issubdrg  19250  sdrgacs  19270  cntzsdrg  19271  abvtriv  19302  islss  19396  lssneln0  19414  lssssr  19415  lbsind  19542  lbspss  19544  lspabs3  19583  lspsneq  19584  lspfixed  19590  lspexch  19591  islbs2  19616  isdomn2  19761  domnrrg  19762  mvrcl  19917  coe1tmmul2  20127  cnflddiv  20257  cnfldinv  20258  xrs1mnd  20265  xrs10  20266  xrge0subm  20268  cnsubdrglem  20278  cnmgpid  20289  cnmsubglem  20290  gzrngunit  20293  zringunit  20317  zringndrg  20319  domnchr  20361  cnmsgngrp  20405  psgninv  20408  psgndiflemB  20426  lindfind  20642  lindsind  20643  lindff1  20646  lindfrn  20647  mdetunilem9  20913  maducoeval2  20933  gsummatr01lem4  20951  ist1-2  21639  cmpfi  21700  2ndcdisj  21748  2ndcsep  21751  locfincmp  21818  alexsublem  22336  cldsubg  22402  imasdsf1olem  22666  prdsxmslem2  22822  reperflem  23109  xrge0gsumle  23124  xrge0tsms  23125  divcn  23159  evth  23246  cvsdiv  23419  cvsdivcl  23420  cphreccllem  23465  bcthlem5  23614  itg11  23975  i1fmullem  23978  i1fadd  23979  itg1addlem2  23981  i1fmulc  23987  itg1mulc  23988  ellimc3  24160  limcmpt2  24165  dvlem  24177  dvidlem  24196  dvcnp  24199  dvcobr  24226  dvrec  24235  dvrecg  24253  dvmptdiv  24254  dvcnvlem  24256  dvexp3  24258  dveflem  24259  dvferm1lem  24264  dvferm2lem  24266  lhop1lem  24293  ftc1lem5  24320  mdegleb  24341  coe1mul3  24376  ply1nz  24398  fta1blem  24445  fta1b  24446  ig1peu  24448  ig1pdvds  24453  plyeq0lem  24483  dgrub  24507  quotval  24564  fta1lem  24579  fta1  24580  elqaalem3  24593  qaa  24595  iaa  24597  aareccl  24598  aannenlem2  24601  abelthlem8  24710  abelth  24712  eff1olem  24813  logrncl  24832  eflog  24841  logeftb  24848  logdmss  24906  dvlog  24915  logbcl  25026  logbid1  25027  logb1  25028  elogb  25029  logbchbase  25030  relogbval  25031  relogbcl  25032  relogbreexp  25034  relogbmul  25036  nnlogbexp  25040  relogbcxp  25044  cxplogb  25045  relogbcxpb  25046  logbf  25048  logblog  25051  2logb9irrALT  25057  sqrt2cxp2logb9e3  25058  angval  25060  dcubic  25105  rlimcnp  25225  efrlim  25229  logexprlim  25483  dchrghm  25514  dchrabs  25518  lgsfcl2  25561  lgsval2lem  25565  lgsval3  25573  lgsmod  25581  lgsdirprm  25589  lgsne0  25593  gausslemma2dlem0f  25619  lgsquad2lem2  25643  2lgsoddprm  25674  2sqlem11  25687  2sqblem  25689  dchrvmaeq0  25762  rpvmasum2  25770  dchrisum0re  25771  qrngdiv  25882  tglngval  26019  tgisline  26095  axlowdimlem9  26419  axlowdimlem12  26422  axlowdimlem13  26423  elntg2  26454  upgrbi  26561  upgr1elem  26580  umgrislfupgrlem  26590  edgupgr  26602  subgruhgredgd  26749  upgrreslem  26769  nbgrel  26805  nbupgr  26809  nbupgrel  26810  nbumgrvtx  26811  nbgrssovtx  26826  nbupgrres  26829  nbusgrvtxm1uvtx  26870  nbupgruvtxres  26872  iscplgredg  26882  cusgredg  26889  cusgrfilem2  26921  usgredgsscusgredg  26924  1loopgrnb0  26967  1egrvtxdg0  26976  uhgrvd00  26999  vtxdginducedm1lem4  27007  eupth2lem3lem3  27691  frcond1  27729  frcond4  27733  2pthfrgr  27747  3cyclfrgrrn1  27748  n4cyclfrgr  27754  frgrwopreglem4a  27773  numclwwlk5  27851  suppss3  30140  xdivval  30271  pmtrcnel  30384  pmtrcnelor  30386  xrge0tsmsd  30495  0nellinds  30575  extdg1id  30649  submatminr1  30682  ordtconnlem1  30776  ispisys2  31021  sigapisys  31023  sibfinima  31206  sseqf  31259  signswch  31440  signstfvn  31448  signsvtn0  31449  signstfvcl  31452  signstfveq0a  31455  signstfveq0  31456  signsvfn  31461  signsvtp  31462  signsvtn  31463  signsvfpn  31464  signsvfnn  31465  signlem0  31466  bnj158  31608  bnj168  31609  bnj529  31621  bnj906  31810  bnj970  31827  exdifsn  31951  cusgredgex2  31973  subfacp1lem5  32033  cvmsi  32114  cvmsval  32115  cvmsdisj  32119  cvmscld  32122  cvmsss2  32123  satfv1lem  32211  sinccvglem  32517  circum  32519  unbdqndv2lem2  33452  bj-0int  34005  lindsadd  34429  lindsenlbs  34431  matunitlindflem2  34433  matunitlindf  34434  poimirlem6  34442  poimirlem7  34443  poimirlem8  34444  poimirlem16  34452  poimirlem18  34454  poimirlem19  34455  poimirlem21  34457  poimirlem22  34458  poimirlem24  34460  poimirlem25  34461  poimirlem26  34462  poimirlem27  34463  itg2addnclem2  34488  sdclem1  34563  rrncmslem  34655  rrnequiv  34658  isdrngo2  34781  isdrngo3  34782  prtlem100  35539  prter2  35561  prter3  35562  lsatlspsn2  35672  lsateln0  35675  lsatn0  35679  lsatspn0  35680  lsatcmp  35683  lsatelbN  35686  islshpat  35697  lsat0cv  35713  lkrlspeqN  35851  dvheveccl  37792  dihlatat  38017  dochnel  38073  dihjat1  38109  dvh4dimlem  38123  dochsnkr2cl  38154  dochkr1  38158  dochkr1OLDN  38159  lcfl6lem  38178  lcfl9a  38185  lclkrlem2l  38198  lclkrlem2o  38201  lclkrlem2q  38203  lcfrlem9  38230  lcfrlem16  38238  lcfrlem17  38239  lcfrlem27  38249  lcfrlem37  38259  lcfrlem38  38260  lcfrlem40  38262  lcdlkreqN  38302  mapdrvallem2  38325  mapdn0  38349  mapdpglem20  38371  mapdpglem30  38382  mapdindp0  38399  mapdhcl  38407  mapdh6aN  38415  mapdh6dN  38419  mapdh6eN  38420  mapdh6kN  38426  mapdh8  38468  hdmap1l6a  38489  hdmap1l6d  38493  hdmap1l6e  38494  hdmap1l6k  38500  hdmapval3N  38518  hdmap10  38520  hdmap11lem2  38522  hdmapnzcl  38525  hdmaprnlem3eN  38538  hdmaprnlem17N  38543  hdmap14lem4a  38551  hdmap14lem7  38554  hdmap14lem14  38561  hgmaprnlem5N  38580  hdmaplkr  38593  hdmapip0  38595  hgmapvvlem2  38604  hgmapvvlem3  38605  hgmapvv  38606  0prjspnlem  38778  pellexlem5  38928  dfac11  39160  dfacbasgrp  39206  dgraalem  39243  dgraaub  39246  aaitgo  39260  proot1ex  39299  isdomn3  39302  deg1mhm  39305  ofdivrec  40209  ofdivcan4  40210  ofdivdiv2  40211  expgrowth  40218  binomcxplemnotnn0  40239  dvdivbd  41763  dvdivcncf  41767  dirkeritg  41943  fourierdlem39  41987  fourierdlem57  42004  fourierdlem58  42005  fourierdlem59  42006  fourierdlem68  42015  fourierdlem76  42023  fourierdlem103  42050  fourierdlem104  42051  fourierdlem111  42058  setsnidel  43067  sprvalpwn0  43141  odz2prm2pw  43221  fmtnoprmfac1  43223  fmtnoprmfac2  43225  sfprmdvdsmersenne  43264  lighneallem2  43267  lighneallem3  43268  lighneal  43272  oddprmALTV  43348  evenprm2  43375  oddprmne2  43376  odd2prm2  43379  even3prm2  43380  2zrngnmrid  43713  lincext1  44003  lindslinindsimp2lem5  44011  rege1logbrege0  44113  fllogbd  44115  relogbmulbexp  44116  relogbdivb  44117  nnpw2blen  44135  blennngt2o2  44147  blennn0e2  44149  dignn0ldlem  44157  line  44214  rrxline  44216  aacllem  44396