Theorem eldifsn 4750

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 3924	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4603	. . . 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 3911  {csn 4589

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 3449  df-dif 3917  df-sn 4590

This theorem is referenced by:  eldifsnd  4751  elpwdifsn  4753  eldifsni  4754  rexdifsn  4758  raldifsni  4759  eldifvsn  4761  difsn  4762  sossfld  6159  tpres  7175  onmindif2  7783  xpord3pred  8131  xpord3inddlem  8133  mptsuppd  8166  suppssr  8174  suppssov1  8176  suppssov2  8177  suppsssn  8180  suppssfv  8181  dif1o  8464  difsnen  9023  limenpsi  9116  frfi  9232  fofinf1o  9283  en2eleq  9961  en2other2  9962  dfac8clem  9985  acni2  9999  acndom  10004  acnnum  10005  dfac9  10090  dfacacn  10095  kmlem3  10106  kmlem4  10107  fin23lem21  10292  canthp1lem2  10606  elni  10829  mulnzcnf  11824  divval  11839  elnnne0  12456  elq  12909  rpcndif0  12972  modfzo0difsn  13908  modsumfzodifsn  13909  expcl2lem  14038  expclzlem  14048  hashdifpr  14380  hashgt23el  14389  prprrab  14438  hashle2prv  14443  reccn2  15563  rlimdiv  15612  eff2  16067  tanval  16096  rpnnen2lem9  16190  fzo0dvdseq  16293  oddprmgt2  16669  oddprmdvds  16874  4sqlem19  16934  prmlem0  17076  prmlem1a  17077  setsnid  17178  grpinvnzcl  18943  symgextf  19347  f1omvdmvd  19373  pmtrprfv  19383  odcau  19534  efgsf  19659  efgsrel  19664  efgs1  19665  efgs1b  19666  efgsp1  19667  efgsres  19668  efgredlema  19670  efgredlemd  19674  efgrelexlemb  19680  gsumpt  19892  dmdprdd  19931  dprdcntz  19940  dprdfeq0  19954  dprd2da  19974  isdomn2OLD  20621  domnrrg  20622  isdomn3  20624  drngunit  20643  isdrng2  20652  drngmcl  20659  drngid2  20661  isdrngd  20674  isdrngdOLD  20676  issubdrg  20689  sdrgacs  20710  cntzsdrg  20711  islss  20840  lssneln0  20859  lssssr  20860  lbsind  20987  lbspss  20989  lspabs3  21031  lspsneq  21032  lspfixed  21038  lspexch  21039  islbs2  21064  cnflddivOLD  21313  cnfldinv  21314  xrs1mnd  21321  xrs10  21322  xrge0subm  21324  cnsubdrglem  21335  cnmgpid  21346  cnmsubglem  21347  gzrngunit  21350  zringunit  21376  zringndrg  21378  domnchr  21442  cnmsgngrp  21488  psgninv  21491  psgndiflemB  21509  lindfind  21725  lindsind  21726  lindff1  21729  lindfrn  21730  mvrcl  21901  coe1tmmul2  22162  mdetunilem9  22507  maducoeval2  22527  gsummatr01lem4  22545  ist1-2  23234  cmpfi  23295  2ndcdisj  23343  2ndcsep  23346  locfincmp  23413  alexsublem  23931  cldsubg  23998  imasdsf1olem  24261  prdsxmslem2  24417  reperflem  24707  xrge0gsumle  24722  xrge0tsms  24723  divcnOLD  24757  divcn  24759  evth  24858  cvsdiv  25032  cvsdivcl  25033  cphreccllem  25078  bcthlem5  25228  itg11  25592  i1fmullem  25595  i1fadd  25596  itg1addlem2  25598  i1fmulc  25604  itg1mulc  25605  ellimc3  25780  limcmpt2  25785  dvlem  25797  dvidlem  25816  dvcnp  25820  dvcobr  25849  dvcobrOLD  25850  dvrec  25859  dvrecg  25877  dvmptdiv  25878  dvcnvlem  25880  dvexp3  25882  dveflem  25883  dvferm1lem  25888  dvferm2lem  25890  lhop1lem  25918  ftc1lem5  25947  mdegleb  25969  coe1mul3  26004  ply1nz  26027  fta1blem  26076  fta1b  26077  ig1peu  26080  ig1pdvds  26085  plyeq0lem  26115  dgrub  26139  quotval  26200  fta1lem  26215  fta1  26216  elqaalem3  26229  qaa  26231  iaa  26233  aareccl  26234  aannenlem2  26237  abelthlem8  26349  abelth  26351  eff1olem  26457  logrncl  26476  eflog  26485  logeftb  26492  logdmss  26551  dvlog  26560  logbcl  26677  logbid1  26678  logb1  26679  elogb  26680  logbchbase  26681  relogbval  26682  relogbcl  26683  relogbreexp  26685  relogbmul  26687  nnlogbexp  26691  relogbcxp  26695  cxplogb  26696  relogbcxpb  26697  logbf  26699  logblog  26702  2logb9irrALT  26708  sqrt2cxp2logb9e3  26709  angval  26711  dcubic  26756  rlimcnp  26875  efrlim  26879  efrlimOLD  26880  logexprlim  27136  dchrghm  27167  dchrabs  27171  lgsfcl2  27214  lgsval2lem  27218  lgsval3  27226  lgsmod  27234  lgsdirprm  27242  lgsne0  27246  gausslemma2dlem0f  27272  lgsquad2lem2  27296  2lgsoddprm  27327  2sqlem11  27340  2sqblem  27342  dchrvmaeq0  27415  rpvmasum2  27423  dchrisum0re  27424  qrngdiv  27535  addsval  27869  divsval  28092  elnns  28232  1nns  28241  tglngval  28478  tgisline  28554  axlowdimlem9  28877  axlowdimlem12  28880  axlowdimlem13  28881  elntg2  28912  upgrbi  29020  upgr1elem  29039  umgrislfupgrlem  29049  edgupgr  29061  subgruhgredgd  29211  upgrreslem  29231  nbgrel  29267  nbupgr  29271  nbupgrel  29272  nbumgrvtx  29273  nbgrssovtx  29288  nbupgrres  29291  nbusgrvtxm1uvtx  29332  nbupgruvtxres  29334  iscplgredg  29344  cusgredg  29351  cusgrfilem2  29384  usgredgsscusgredg  29387  1loopgrnb0  29430  1egrvtxdg0  29439  uhgrvd00  29462  vtxdginducedm1lem4  29470  eupth2lem3lem3  30159  frcond1  30195  frcond4  30199  2pthfrgr  30213  3cyclfrgrrn1  30214  n4cyclfrgr  30220  frgrwopreglem4a  30239  numclwwlk5  30317  ressupprn  32613  suppss3  32647  xdivval  32839  xrge0tsmsd  33002  pmtrcnel  33046  pmtrcnelor  33048  0nellinds  33341  dvdsruasso  33356  mxidlirredi  33442  extdg1id  33661  irngnzply1  33686  submatminr1  33800  ordtconnlem1  33914  ispisys2  34143  sigapisys  34145  sibfinima  34330  sseqf  34383  signswch  34552  signstfvn  34560  signsvtn0  34561  signstfvneq0  34563  signstfvcl  34564  signstfveq0a  34567  signstfveq0  34568  signsvfn  34573  signsvtp  34574  signsvtn  34575  signsvfpn  34576  signsvfnn  34577  signlem0  34578  bnj158  34719  bnj168  34720  bnj529  34731  bnj906  34920  bnj970  34937  exdifsn  35069  cusgredgex2  35110  subfacp1lem5  35171  cvmsi  35252  cvmsval  35253  cvmsdisj  35257  cvmscld  35260  cvmsss2  35261  satfv1lem  35349  sinccvglem  35659  circum  35661  mpomulnzcnf  36287  unbdqndv2lem2  36498  bj-0int  37089  lindsadd  37607  lindsenlbs  37609  matunitlindflem2  37611  matunitlindf  37612  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem16  37630  poimirlem18  37632  poimirlem19  37633  poimirlem21  37635  poimirlem22  37636  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  itg2addnclem2  37666  sdclem1  37737  rrncmslem  37826  rrnequiv  37829  isdrngo2  37952  isdrngo3  37953  eldmxrncnvepres  38396  eldmxrncnvepres2  38397  prtlem100  38852  prter2  38874  prter3  38875  lsatlspsn2  38985  lsateln0  38988  lsatn0  38992  lsatspn0  38993  lsatcmp  38996  lsatelbN  38999  islshpat  39010  lsat0cv  39026  lkrlspeqN  39164  dvheveccl  41106  dihlatat  41331  dochnel  41387  dihjat1  41423  dvh4dimlem  41437  dochsnkr2cl  41468  dochkr1  41472  dochkr1OLDN  41473  lcfl6lem  41492  lcfl9a  41499  lclkrlem2l  41512  lclkrlem2o  41515  lclkrlem2q  41517  lcfrlem9  41544  lcfrlem16  41552  lcfrlem17  41553  lcfrlem27  41563  lcfrlem37  41573  lcfrlem38  41574  lcfrlem40  41576  lcdlkreqN  41616  mapdrvallem2  41639  mapdn0  41663  mapdpglem20  41685  mapdpglem30  41696  mapdindp0  41713  mapdhcl  41721  mapdh6aN  41729  mapdh6dN  41733  mapdh6eN  41734  mapdh6kN  41740  mapdh8  41782  hdmap1l6a  41803  hdmap1l6d  41807  hdmap1l6e  41808  hdmap1l6k  41814  hdmapval3N  41832  hdmap10  41834  hdmap11lem2  41836  hdmapnzcl  41839  hdmaprnlem3eN  41852  hdmaprnlem17N  41857  hdmap14lem4a  41865  hdmap14lem7  41868  hdmap14lem14  41875  hgmaprnlem5N  41894  hdmaplkr  41907  hdmapip0  41909  hgmapvvlem2  41918  hgmapvvlem3  41919  hgmapvv  41920  redvmptabs  42348  readvrec2  42349  readvrec  42350  fiabv  42524  fsuppind  42578  0prjspnlem  42611  pellexlem5  42821  dfac11  43051  dfacbasgrp  43097  dgraalem  43134  dgraaub  43137  aaitgo  43151  proot1ex  43185  deg1mhm  43189  ofdivrec  44315  ofdivcan4  44316  ofdivdiv2  44317  expgrowth  44324  binomcxplemnotnn0  44345  dvdivbd  45921  dvdivcncf  45925  dirkeritg  46100  fourierdlem39  46144  fourierdlem57  46161  fourierdlem58  46162  fourierdlem59  46163  fourierdlem68  46172  fourierdlem76  46180  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  setsnidel  47378  sprvalpwn0  47484  odz2prm2pw  47564  fmtnoprmfac1  47566  fmtnoprmfac2  47568  sfprmdvdsmersenne  47604  lighneallem2  47607  lighneallem3  47608  lighneal  47612  oddprmALTV  47688  evenprm2  47715  oddprmne2  47716  odd2prm2  47719  even3prm2  47720  isubgruhgr  47868  grimuhgr  47887  2zrngnmrid  48244  lincext1  48443  lindslinindsimp2lem5  48451  rege1logbrege0  48547  fllogbd  48549  relogbmulbexp  48550  relogbdivb  48551  nnpw2blen  48569  blennngt2o2  48581  blennn0e2  48583  dignn0ldlem  48591  line  48721  rrxline  48723  aacllem  49790