Theorem eldifsn 4756

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 3921	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4606	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 3001	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 584	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 278	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   ∈ wcel 2149   ≠ wne 2964   ∖ cdif 3908  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-v 3463  df-dif 3914  df-sn 4593

This theorem is referenced by:  eldifsnd  4757  eldifsni  4760  rexdifsn  4764  raldifsni  4765  eldifvsn  4767  difsn  4768  sossfld  6185  tpres  7200  onmindif2  7806  xpord3pred  8148  xpord3inddlem  8150  mptsuppd  8183  suppssr  8191  suppssov1  8193  suppssov2  8194  suppsssn  8197  suppssfv  8198  dif1o  8485  difsnen  9047  limenpsi  9140  frfi  9245  fofinf1o  9289  en2eleq  9992  en2other2  9993  dfac8clem  10016  acni2  10030  acndom  10035  acnnum  10036  dfac9  10120  dfacacn  10125  kmlem3  10136  kmlem4  10137  fin23lem21  10323  canthp1lem2  10638  elni  10861  mulnzcnf  11860  divval  11874  elnnne0  12518  elq  12974  rpcndif0  13037  modfzo0difsn  13979  modsumfzodifsn  13980  expcl2lem  14109  expclzlem  14119  hashdifpr  14452  hashgt23el  14461  prprrab  14510  hashle2prv  14515  reccn2  15648  rlimdiv  15697  eff2  16155  tanval  16184  rpnnen2lem9  16278  fzo0dvdseq  16381  oddprmgt2  16758  oddprmdvds  16963  4sqlem19  17023  prmlem0  17165  prmlem1a  17166  setsnid  17268  grpinvnzcl  19077  symgextf  19487  f1omvdmvd  19513  pmtrprfv  19523  odcau  19674  efgsf  19799  efgsrel  19804  efgs1  19805  efgs1b  19806  efgsp1  19807  efgsres  19808  efgredlema  19810  efgredlemd  19814  efgrelexlemb  19820  gsumpt  20032  dmdprdd  20071  dprdcntz  20080  dprdfeq0  20094  dprd2da  20114  domnrrg  20797  isdomn3  20799  drngunit  20818  isdrng2  20827  drngmcl  20834  drngid2  20835  isdrngd  20847  isdrngdOLD  20849  issubdrg  20861  sdrgacs  20882  cntzsdrg  20883  islss  21033  lssneln0  21052  lssssr  21053  lbsind  21179  lbspss  21181  lspabs3  21223  lspsneq  21224  lspfixed  21230  lspexch  21231  islbs2  21256  cnfldinv  21522  cnsubdrglem  21537  cnmgpid  21548  cnmsubglem  21549  gzrngunit  21552  xrs1mnd  21559  xrs10  21560  xrge0subm  21562  zringunit  21585  zringndrg  21587  domnchr  21651  cnmsgngrp  21698  psgninv  21701  psgndiflemB  21719  lindfind  21935  lindsind  21936  lindff1  21939  lindfrn  21940  mvrcl  22110  coe1tmmul2  22406  mdetunilem9  22746  maducoeval2  22766  gsummatr01lem4  22784  ist1-2  23473  cmpfi  23534  2ndcdisj  23582  2ndcsep  23585  locfincmp  23652  alexsublem  24170  cldsubg  24237  imasdsf1olem  24499  prdsxmslem2  24655  reperflem  24945  xrge0gsumle  24960  xrge0tsms  24961  divcn  24996  evth  25087  cvsdiv  25260  cvsdivcl  25261  cphreccllem  25306  bcthlem5  25456  itg11  25819  i1fmullem  25822  i1fadd  25823  itg1addlem2  25825  i1fmulc  25831  itg1mulc  25832  ellimc3  26007  limcmpt2  26012  dvlem  26024  dvidlem  26043  dvcnp  26047  dvcobr  26074  dvrec  26083  dvrecg  26101  dvmptdiv  26102  dvcnvlem  26104  dvexp3  26106  dveflem  26107  dvferm1lem  26112  dvferm2lem  26114  lhop1lem  26141  ftc1lem5  26168  mdegleb  26190  coe1mul3  26225  ply1nz  26248  fta1blem  26297  fta1b  26298  ig1peu  26301  ig1pdvds  26306  plyeq0lem  26336  dgrub  26360  quotval  26422  fta1lem  26437  fta1  26438  elqaalem3  26451  qaa  26453  iaa  26455  aareccl  26456  aannenlem2  26459  abelthlem8  26568  abelth  26570  eff1olem  26679  logrncl  26698  eflog  26707  logeftb  26714  logdmss  26773  dvlog  26782  logbcl  26898  logbid1  26899  logb1  26900  elogb  26901  logbchbase  26902  relogbval  26903  relogbcl  26904  relogbreexp  26906  relogbmul  26908  nnlogbexp  26912  relogbcxp  26916  cxplogb  26917  relogbcxpb  26918  logbf  26920  logblog  26923  2logb9irrALT  26929  sqrt2cxp2logb9e3  26930  angval  26932  dcubic  26977  rlimcnp  27096  efrlim  27100  logexprlim  27355  dchrghm  27386  dchrabs  27390  lgsfcl2  27433  lgsval2lem  27437  lgsval3  27445  lgsmod  27453  lgsdirprm  27461  lgsne0  27465  gausslemma2dlem0f  27491  lgsquad2lem2  27515  2lgsoddprm  27546  2sqlem11  27559  2sqblem  27561  dchrvmaeq0  27634  rpvmasum2  27642  dchrisum0re  27643  qrngdiv  27754  addsval  28121  divsval  28348  elnns  28499  1nns  28508  tglngval  28786  tgisline  28862  axlowdimlem9  29241  axlowdimlem12  29244  axlowdimlem13  29245  elntg2  29276  upgrbi  29384  upgr1elem  29403  umgrislfupgrlem  29413  edgupgr  29425  subgruhgredgd  29575  upgrreslem  29595  nbgrel  29631  nbupgr  29635  nbupgrel  29636  nbumgrvtx  29637  nbgrssovtx  29652  nbupgrres  29655  nbusgrvtxm1uvtx  29696  nbupgruvtxres  29698  iscplgredg  29708  cusgredg  29715  cusgrfilem2  29747  usgredgsscusgredg  29750  1loopgrnb0  29793  1egrvtxdg0  29802  uhgrvd00  29825  vtxdginducedm1lem4  29833  eupth2lem3lem3  30522  frcond1  30558  frcond4  30562  2pthfrgr  30576  3cyclfrgrrn1  30577  n4cyclfrgr  30583  frgrwopreglem4a  30602  numclwwlk5  30680  ressupprn  32976  suppss3  33009  xdivval  33179  xrge0tsmsd  33334  pmtrcnel  33350  pmtrcnelor  33352  0nellinds  33628  dvdsruasso  33642  extdg1id  34001  irngnzply1  34026  submatminr1  34145  ordtconnlem1  34259  ispisys2  34488  sigapisys  34490  sibfinima  34674  sseqf  34727  signswch  34893  signstfvn  34901  signsvtn0  34902  signstfvneq0  34904  signstfvcl  34905  signstfveq0a  34908  signstfveq0  34909  signsvfn  34914  signsvtp  34915  signsvtn  34916  signsvfpn  34917  signsvfnn  34918  signlem0  34919  bnj158  35063  bnj168  35064  bnj529  35075  bnj906  35263  bnj970  35280  exdifsn  35412  cusgredgex2  35548  subfacp1lem5  35609  cvmsi  35690  cvmsval  35691  cvmsdisj  35695  cvmscld  35698  cvmsss2  35699  satfv1lem  35787  sinccvglem  36097  circum  36099  mpomulnzcnf  36734  unbdqndv2lem2  37022  bj-0int  37666  lindsadd  38187  lindsenlbs  38189  matunitlindflem2  38191  matunitlindf  38192  poimirlem6  38200  poimirlem7  38201  poimirlem8  38202  poimirlem16  38210  poimirlem18  38212  poimirlem19  38213  poimirlem21  38215  poimirlem22  38216  poimirlem24  38218  poimirlem25  38219  poimirlem26  38220  poimirlem27  38221  itg2addnclem2  38246  sdclem1  38317  rrncmslem  38406  rrnequiv  38409  isdrngo2  38532  isdrngo3  38533  eldmxrncnvepres  39008  eldmxrncnvepres2  39009  prtlem100  39558  prter2  39580  prter3  39581  lsatlspsn2  39691  lsateln0  39694  lsatn0  39698  lsatspn0  39699  lsatcmp  39702  lsatelbN  39705  islshpat  39716  lsat0cv  39732  lkrlspeqN  39870  dvheveccl  41811  dihlatat  42036  dochnel  42092  dihjat1  42128  dvh4dimlem  42142  dochsnkr2cl  42173  dochkr1  42177  dochkr1OLDN  42178  lcfl6lem  42197  lcfl9a  42204  lclkrlem2l  42217  lclkrlem2o  42220  lclkrlem2q  42222  lcfrlem9  42249  lcfrlem16  42257  lcfrlem17  42258  lcfrlem27  42268  lcfrlem37  42278  lcfrlem38  42279  lcfrlem40  42281  lcdlkreqN  42321  mapdrvallem2  42344  mapdn0  42368  mapdpglem20  42390  mapdpglem30  42401  mapdindp0  42418  mapdhcl  42426  mapdh6aN  42434  mapdh6dN  42438  mapdh6eN  42439  mapdh6kN  42445  mapdh8  42487  hdmap1l6a  42508  hdmap1l6d  42512  hdmap1l6e  42513  hdmap1l6k  42519  hdmapval3N  42537  hdmap10  42539  hdmap11lem2  42541  hdmapnzcl  42544  hdmaprnlem3eN  42557  hdmaprnlem17N  42562  hdmap14lem4a  42570  hdmap14lem7  42573  hdmap14lem14  42580  hgmaprnlem5N  42599  hdmaplkr  42612  hdmapip0  42614  hgmapvvlem2  42623  hgmapvvlem3  42624  hgmapvv  42625  redvmptabs  43046  readvrec2  43047  readvrec  43048  fiabv  43231  fsuppind  43249  0prjspnlem  43282  pellexlem5  43487  dfac11  43716  dfacbasgrp  43762  dgraalem  43799  dgraaub  43802  aaitgo  43816  proot1ex  43850  deg1mhm  43854  ofdivrec  44963  ofdivcan4  44964  ofdivdiv2  44965  expgrowth  44972  binomcxplemnotnn0  44993  dvdivbd  46564  dvdivcncf  46568  dirkeritg  46743  fourierdlem39  46787  fourierdlem57  46804  fourierdlem58  46805  fourierdlem59  46806  fourierdlem68  46815  fourierdlem76  46823  fourierdlem103  46850  fourierdlem104  46851  fourierdlem111  46858  setsnidel  48050  sprvalpwn0  48156  odz2prm2pw  48239  fmtnoprmfac1  48241  fmtnoprmfac2  48243  sfprmdvdsmersenne  48279  lighneallem2  48282  lighneallem3  48283  lighneal  48287  oddprmALTV  48376  evenprm2  48403  oddprmne2  48404  odd2prm2  48407  even3prm2  48408  isubgruhgr  48557  grimuhgr  48576  2zrngnmrid  48945  lincext1  49154  lindslinindsimp2lem5  49162  rege1logbrege0  49258  fllogbd  49260  relogbmulbexp  49261  relogbdivb  49262  nnpw2blen  49280  blennngt2o2  49292  blennn0e2  49294  dignn0ldlem  49302  line  49432  rrxline  49434  aacllem  50510