Theorem eldifsn 4762

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   ≠ wne 2932   ∖ cdif 3923  {csn 4601

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-sn 4602

This theorem is referenced by:  eldifsnd  4763  elpwdifsn  4765  eldifsni  4766  rexdifsn  4770  raldifsni  4771  eldifvsn  4773  difsn  4774  sossfld  6175  tpres  7192  onmindif2  7799  xpord3pred  8149  xpord3inddlem  8151  mptsuppd  8184  suppssr  8192  suppssov1  8194  suppssov2  8195  suppsssn  8198  suppssfv  8199  dif1o  8510  difsnen  9065  limenpsi  9164  frfi  9291  fofinf1o  9342  en2eleq  10020  en2other2  10021  dfac8clem  10044  acni2  10058  acndom  10063  acnnum  10064  dfac9  10149  dfacacn  10154  kmlem3  10165  kmlem4  10166  fin23lem21  10351  canthp1lem2  10665  elni  10888  mulnzcnf  11881  divval  11896  elnnne0  12513  elq  12964  rpcndif0  13026  modfzo0difsn  13959  modsumfzodifsn  13960  expcl2lem  14089  expclzlem  14099  hashdifpr  14431  hashgt23el  14440  prprrab  14489  hashle2prv  14494  reccn2  15611  rlimdiv  15660  eff2  16115  tanval  16144  rpnnen2lem9  16238  fzo0dvdseq  16340  oddprmgt2  16716  oddprmdvds  16921  4sqlem19  16981  prmlem0  17123  prmlem1a  17124  setsnid  17225  grpinvnzcl  18992  symgextf  19396  f1omvdmvd  19422  pmtrprfv  19432  odcau  19583  efgsf  19708  efgsrel  19713  efgs1  19714  efgs1b  19715  efgsp1  19716  efgsres  19717  efgredlema  19719  efgredlemd  19723  efgrelexlemb  19729  gsumpt  19941  dmdprdd  19980  dprdcntz  19989  dprdfeq0  20003  dprd2da  20023  isdomn2OLD  20670  domnrrg  20671  isdomn3  20673  drngunit  20692  isdrng2  20701  drngmcl  20708  drngid2  20710  isdrngd  20723  isdrngdOLD  20725  issubdrg  20738  sdrgacs  20759  cntzsdrg  20760  islss  20889  lssneln0  20908  lssssr  20909  lbsind  21036  lbspss  21038  lspabs3  21080  lspsneq  21081  lspfixed  21087  lspexch  21088  islbs2  21113  cnflddivOLD  21362  cnfldinv  21363  xrs1mnd  21370  xrs10  21371  xrge0subm  21373  cnsubdrglem  21384  cnmgpid  21395  cnmsubglem  21396  gzrngunit  21399  zringunit  21425  zringndrg  21427  domnchr  21491  cnmsgngrp  21537  psgninv  21540  psgndiflemB  21558  lindfind  21774  lindsind  21775  lindff1  21778  lindfrn  21779  mvrcl  21950  coe1tmmul2  22211  mdetunilem9  22556  maducoeval2  22576  gsummatr01lem4  22594  ist1-2  23283  cmpfi  23344  2ndcdisj  23392  2ndcsep  23395  locfincmp  23462  alexsublem  23980  cldsubg  24047  imasdsf1olem  24310  prdsxmslem2  24466  reperflem  24756  xrge0gsumle  24771  xrge0tsms  24772  divcnOLD  24806  divcn  24808  evth  24907  cvsdiv  25081  cvsdivcl  25082  cphreccllem  25128  bcthlem5  25278  itg11  25642  i1fmullem  25645  i1fadd  25646  itg1addlem2  25648  i1fmulc  25654  itg1mulc  25655  ellimc3  25830  limcmpt2  25835  dvlem  25847  dvidlem  25866  dvcnp  25870  dvcobr  25899  dvcobrOLD  25900  dvrec  25909  dvrecg  25927  dvmptdiv  25928  dvcnvlem  25930  dvexp3  25932  dveflem  25933  dvferm1lem  25938  dvferm2lem  25940  lhop1lem  25968  ftc1lem5  25997  mdegleb  26019  coe1mul3  26054  ply1nz  26077  fta1blem  26126  fta1b  26127  ig1peu  26130  ig1pdvds  26135  plyeq0lem  26165  dgrub  26189  quotval  26250  fta1lem  26265  fta1  26266  elqaalem3  26279  qaa  26281  iaa  26283  aareccl  26284  aannenlem2  26287  abelthlem8  26399  abelth  26401  eff1olem  26507  logrncl  26526  eflog  26535  logeftb  26542  logdmss  26601  dvlog  26610  logbcl  26727  logbid1  26728  logb1  26729  elogb  26730  logbchbase  26731  relogbval  26732  relogbcl  26733  relogbreexp  26735  relogbmul  26737  nnlogbexp  26741  relogbcxp  26745  cxplogb  26746  relogbcxpb  26747  logbf  26749  logblog  26752  2logb9irrALT  26758  sqrt2cxp2logb9e3  26759  angval  26761  dcubic  26806  rlimcnp  26925  efrlim  26929  efrlimOLD  26930  logexprlim  27186  dchrghm  27217  dchrabs  27221  lgsfcl2  27264  lgsval2lem  27268  lgsval3  27276  lgsmod  27284  lgsdirprm  27292  lgsne0  27296  gausslemma2dlem0f  27322  lgsquad2lem2  27346  2lgsoddprm  27377  2sqlem11  27390  2sqblem  27392  dchrvmaeq0  27465  rpvmasum2  27473  dchrisum0re  27474  qrngdiv  27585  addsval  27912  divsval  28132  elnns  28260  1nns  28269  tglngval  28476  tgisline  28552  axlowdimlem9  28875  axlowdimlem12  28878  axlowdimlem13  28879  elntg2  28910  upgrbi  29018  upgr1elem  29037  umgrislfupgrlem  29047  edgupgr  29059  subgruhgredgd  29209  upgrreslem  29229  nbgrel  29265  nbupgr  29269  nbupgrel  29270  nbumgrvtx  29271  nbgrssovtx  29286  nbupgrres  29289  nbusgrvtxm1uvtx  29330  nbupgruvtxres  29332  iscplgredg  29342  cusgredg  29349  cusgrfilem2  29382  usgredgsscusgredg  29385  1loopgrnb0  29428  1egrvtxdg0  29437  uhgrvd00  29460  vtxdginducedm1lem4  29468  eupth2lem3lem3  30157  frcond1  30193  frcond4  30197  2pthfrgr  30211  3cyclfrgrrn1  30212  n4cyclfrgr  30218  frgrwopreglem4a  30237  numclwwlk5  30315  ressupprn  32613  suppss3  32647  xdivval  32839  xrge0tsmsd  33002  pmtrcnel  33046  pmtrcnelor  33048  0nellinds  33331  dvdsruasso  33346  mxidlirredi  33432  extdg1id  33653  irngnzply1  33678  submatminr1  33787  ordtconnlem1  33901  ispisys2  34130  sigapisys  34132  sibfinima  34317  sseqf  34370  signswch  34539  signstfvn  34547  signsvtn0  34548  signstfvneq0  34550  signstfvcl  34551  signstfveq0a  34554  signstfveq0  34555  signsvfn  34560  signsvtp  34561  signsvtn  34562  signsvfpn  34563  signsvfnn  34564  signlem0  34565  bnj158  34706  bnj168  34707  bnj529  34718  bnj906  34907  bnj970  34924  exdifsn  35056  cusgredgex2  35091  subfacp1lem5  35152  cvmsi  35233  cvmsval  35234  cvmsdisj  35238  cvmscld  35241  cvmsss2  35242  satfv1lem  35330  sinccvglem  35640  circum  35642  mpomulnzcnf  36263  unbdqndv2lem2  36474  bj-0int  37065  lindsadd  37583  lindsenlbs  37585  matunitlindflem2  37587  matunitlindf  37588  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem16  37606  poimirlem18  37608  poimirlem19  37609  poimirlem21  37611  poimirlem22  37612  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  itg2addnclem2  37642  sdclem1  37713  rrncmslem  37802  rrnequiv  37805  isdrngo2  37928  isdrngo3  37929  prtlem100  38823  prter2  38845  prter3  38846  lsatlspsn2  38956  lsateln0  38959  lsatn0  38963  lsatspn0  38964  lsatcmp  38967  lsatelbN  38970  islshpat  38981  lsat0cv  38997  lkrlspeqN  39135  dvheveccl  41077  dihlatat  41302  dochnel  41358  dihjat1  41394  dvh4dimlem  41408  dochsnkr2cl  41439  dochkr1  41443  dochkr1OLDN  41444  lcfl6lem  41463  lcfl9a  41470  lclkrlem2l  41483  lclkrlem2o  41486  lclkrlem2q  41488  lcfrlem9  41515  lcfrlem16  41523  lcfrlem17  41524  lcfrlem27  41534  lcfrlem37  41544  lcfrlem38  41545  lcfrlem40  41547  lcdlkreqN  41587  mapdrvallem2  41610  mapdn0  41634  mapdpglem20  41656  mapdpglem30  41667  mapdindp0  41684  mapdhcl  41692  mapdh6aN  41700  mapdh6dN  41704  mapdh6eN  41705  mapdh6kN  41711  mapdh8  41753  hdmap1l6a  41774  hdmap1l6d  41778  hdmap1l6e  41779  hdmap1l6k  41785  hdmapval3N  41803  hdmap10  41805  hdmap11lem2  41807  hdmapnzcl  41810  hdmaprnlem3eN  41823  hdmaprnlem17N  41828  hdmap14lem4a  41836  hdmap14lem7  41839  hdmap14lem14  41846  hgmaprnlem5N  41865  hdmaplkr  41878  hdmapip0  41880  hgmapvvlem2  41889  hgmapvvlem3  41890  hgmapvv  41891  redvmptabs  42350  readvrec2  42351  readvrec  42352  fiabv  42506  fsuppind  42560  0prjspnlem  42593  pellexlem5  42803  dfac11  43033  dfacbasgrp  43079  dgraalem  43116  dgraaub  43119  aaitgo  43133  proot1ex  43167  deg1mhm  43171  ofdivrec  44298  ofdivcan4  44299  ofdivdiv2  44300  expgrowth  44307  binomcxplemnotnn0  44328  dvdivbd  45900  dvdivcncf  45904  dirkeritg  46079  fourierdlem39  46123  fourierdlem57  46140  fourierdlem58  46141  fourierdlem59  46142  fourierdlem68  46151  fourierdlem76  46159  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  setsnidel  47339  sprvalpwn0  47445  odz2prm2pw  47525  fmtnoprmfac1  47527  fmtnoprmfac2  47529  sfprmdvdsmersenne  47565  lighneallem2  47568  lighneallem3  47569  lighneal  47573  oddprmALTV  47649  evenprm2  47676  oddprmne2  47677  odd2prm2  47680  even3prm2  47681  isubgruhgr  47829  grimuhgr  47848  2zrngnmrid  48179  lincext1  48378  lindslinindsimp2lem5  48386  rege1logbrege0  48486  fllogbd  48488  relogbmulbexp  48489  relogbdivb  48490  nnpw2blen  48508  blennngt2o2  48520  blennn0e2  48522  dignn0ldlem  48530  line  48660  rrxline  48662  aacllem  49613