Theorem eldifsn 4535

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 3807	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4410	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 3035	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 572	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 267	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 386   ∈ wcel 2166   ≠ wne 2998   ∖ cdif 3794  {csn 4396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-v 3415  df-dif 3800  df-sn 4397

This theorem is referenced by:  ssdifsnOLD  4537  elpwdifsn  4538  eldifsni  4539  rexdifsn  4542  raldifsni  4543  eldifvsn  4545  difsn  4546  prproe  4655  sossfld  5820  tpres  6721  mpt2difsnif  7012  onmindif2  7272  mptsuppd  7581  suppssr  7590  suppssov1  7591  suppsssn  7594  suppssfv  7595  dif1o  7846  difsnen  8310  limenpsi  8403  frfi  8473  fofinf1o  8509  wemapso2lem  8725  en2eleq  9143  en2other2  9144  dfac8clem  9167  acni2  9181  acndom  9186  acnnum  9187  dfac9  9272  dfacacn  9277  kmlem3  9288  kmlem4  9289  fin23lem21  9475  canthp1lem2  9789  elni  10012  mulnzcnopr  10997  divval  11011  elnnne0  11633  elq  12072  rpcndif0  12132  modfzo0difsn  13036  modsumfzodifsn  13037  expcl2lem  13165  expclzlem  13177  hashdifpr  13491  prprrab  13543  hashle2prv  13548  reccn2  14703  rlimdiv  14752  eff2  15200  tanval  15229  rpnnen2lem9  15324  fzo0dvdseq  15421  oddprmgt2  15782  oddprmdvds  15977  4sqlem19  16037  prmlem0  16177  prmlem1a  16178  setsnid  16277  grpinvnzcl  17840  symgextf  18186  symgextfv  18187  f1omvdmvd  18212  pmtrprfv  18222  odcau  18369  efgsf  18492  efgsrel  18497  efgs1  18498  efgs1b  18499  efgsp1  18500  efgsres  18501  efgsresOLD  18502  efgredlema  18504  efgredlemd  18508  efgrelexlemb  18515  gsumpt  18713  dmdprdd  18751  dprdcntz  18760  dprdfeq0  18774  dprd2da  18794  drngunit  19107  isdrng2  19112  drngid2  19118  isdrngd  19127  issubdrg  19160  abvtriv  19196  islss  19290  lssneln0  19308  lssneln0OLD  19309  lssssr  19310  lssssrOLD  19311  lbsind  19438  lbspss  19440  lspabs3  19479  lspsneq  19480  lspfixed  19486  lspfixedOLD  19487  lspexch  19488  islbs2  19514  isdomn2  19659  domnrrg  19660  mvrcl  19809  coe1tmmul2  20005  cnflddiv  20135  cnfldinv  20136  xrs1mnd  20143  xrs10  20144  xrge0subm  20146  cnsubdrglem  20156  cnmgpid  20167  cnmsubglem  20168  gzrngunit  20171  zringunit  20195  zringndrg  20197  domnchr  20239  cnmsgngrp  20283  psgninv  20286  psgndiflemB  20305  lindfind  20521  lindsind  20522  lindff1  20525  lindfrn  20526  mdetunilem9  20793  maducoeval2  20813  gsummatr01lem4  20832  ist1-2  21521  cmpfi  21581  2ndcdisj  21629  2ndcsep  21632  locfincmp  21699  alexsublem  22217  cldsubg  22283  imasdsf1olem  22547  prdsxmslem2  22703  reperflem  22990  xrge0gsumle  23005  xrge0tsms  23006  divcn  23040  evth  23127  cvsdiv  23300  cvsdivcl  23301  cphreccllem  23346  bcthlem5  23495  itg11  23856  i1fmullem  23859  i1fadd  23860  itg1addlem2  23862  i1fmulc  23868  itg1mulc  23869  ellimc3  24041  limcmpt2  24046  dvlem  24058  dvidlem  24077  dvcnp  24080  dvcobr  24107  dvrec  24116  dvrecg  24134  dvmptdiv  24135  dvcnvlem  24137  dvexp3  24139  dveflem  24140  dvferm1lem  24145  dvferm2lem  24147  lhop1lem  24174  ftc1lem5  24201  mdegleb  24222  coe1mul3  24257  ply1nz  24279  fta1blem  24326  fta1b  24327  ig1peu  24329  ig1pdvds  24334  plyeq0lem  24364  dgrub  24388  quotval  24445  fta1lem  24460  fta1  24461  elqaalem3  24474  qaa  24476  iaa  24478  aareccl  24479  aannenlem2  24482  abelthlem8  24591  abelth  24593  reefgim  24602  eff1olem  24693  logrncl  24712  eflog  24721  logeftb  24728  logdmss  24786  dvlog  24795  logbcl  24906  logbid1  24907  logb1  24908  elogb  24909  logbchbase  24910  relogbval  24911  relogbcl  24912  relogbreexp  24914  relogbmul  24916  nnlogbexp  24920  relogbcxp  24924  cxplogb  24925  relogbcxpb  24926  logbf  24928  logblog  24931  2logb9irrALT  24937  sqrt2cxp2logb9e3  24938  angval  24940  dcubic  24985  rlimcnp  25104  efrlim  25108  logexprlim  25362  dchrghm  25393  dchrabs  25397  lgsfcl2  25440  lgsval2lem  25444  lgsval3  25452  lgsmod  25460  lgsdirprm  25468  lgsne0  25472  gausslemma2dlem0f  25498  lgsquad2lem2  25522  2lgsoddprm  25553  2sqlem11  25566  2sqblem  25568  dchrvmaeq0  25605  rpvmasum2  25613  dchrisum0re  25614  qrngdiv  25725  tglngval  25862  tgisline  25938  axlowdimlem9  26248  axlowdimlem12  26251  axlowdimlem13  26252  elntg2  26283  upgrbi  26390  upgr1elem  26409  umgrislfupgrlem  26419  edgupgr  26431  subgruhgredgd  26580  upgrreslem  26600  nbgrel  26636  nbupgr  26640  nbupgrel  26641  nbumgrvtx  26642  nbgrssovtx  26657  nbupgrres  26660  nbusgrvtxm1uvtx  26702  nbupgruvtxres  26704  iscplgredg  26714  cusgredg  26721  cusgrfilem2  26753  usgredgsscusgredg  26756  1loopgrnb0  26799  1egrvtxdg0  26808  uhgrvd00  26831  vtxdginducedm1lem4  26839  eupth2lem3lem3  27606  frcond1  27646  frcond4  27650  2pthfrgr  27664  3cyclfrgrrn1  27665  n4cyclfrgr  27671  frgrwopreglem4a  27690  numclwwlk5  27802  suppss3  30049  xdivval  30171  xrge0tsmsd  30329  submatminr1  30420  ordtconnlem1  30514  ispisys2  30760  sigapisys  30762  sibfinima  30945  sseqf  30999  signswch  31184  signstfvn  31192  signsvtn0  31193  signsvtn0OLD  31194  signstfvcl  31197  signstfveq0a  31200  signstfveq0  31201  signstfveq0OLD  31202  signsvfn  31207  signsvtp  31208  signsvtn  31209  signsvfpn  31210  signsvfnn  31211  signlem0  31212  bnj158  31343  bnj168  31344  bnj529  31356  bnj906  31545  bnj970  31562  subfacp1lem5  31711  cvmsi  31792  cvmsval  31793  cvmsdisj  31797  cvmscld  31800  cvmsss2  31801  sinccvglem  32109  circum  32111  unbdqndv2lem2  33032  bj-0int  33577  lindsadd  33945  lindsenlbs  33947  matunitlindflem2  33949  matunitlindf  33950  poimirlem6  33958  poimirlem7  33959  poimirlem8  33960  poimirlem16  33968  poimirlem18  33970  poimirlem19  33971  poimirlem21  33973  poimirlem22  33974  poimirlem24  33976  poimirlem25  33977  poimirlem26  33978  poimirlem27  33979  itg2addnclem2  34004  sdclem1  34080  rrncmslem  34172  rrnequiv  34175  isdrngo2  34298  isdrngo3  34299  prtlem100  34933  prter2  34955  prter3  34956  lsatlspsn2  35066  lsateln0  35069  lsatn0  35073  lsatspn0  35074  lsatcmp  35077  lsatelbN  35080  islshpat  35091  lsat0cv  35107  lkrlspeqN  35245  dvheveccl  37186  dihlatat  37411  dochnel  37467  dihjat1  37503  dvh4dimlem  37517  dochsnkr2cl  37548  dochkr1  37552  dochkr1OLDN  37553  lcfl6lem  37572  lcfl9a  37579  lclkrlem2l  37592  lclkrlem2o  37595  lclkrlem2q  37597  lcfrlem9  37624  lcfrlem16  37632  lcfrlem17  37633  lcfrlem27  37643  lcfrlem37  37653  lcfrlem38  37654  lcfrlem40  37656  lcdlkreqN  37696  mapdrvallem2  37719  mapdn0  37743  mapdpglem20  37765  mapdpglem30  37776  mapdindp0  37793  mapdhcl  37801  mapdh6aN  37809  mapdh6dN  37813  mapdh6eN  37814  mapdh6kN  37820  mapdh8  37862  hdmap1l6a  37883  hdmap1l6d  37887  hdmap1l6e  37888  hdmap1l6k  37894  hdmapval3N  37912  hdmap10  37914  hdmap11lem2  37916  hdmapnzcl  37919  hdmaprnlem3eN  37932  hdmaprnlem17N  37937  hdmap14lem4a  37945  hdmap14lem7  37948  hdmap14lem14  37955  hgmaprnlem5N  37974  hdmaplkr  37987  hdmapip0  37989  hgmapvvlem2  37998  hgmapvvlem3  37999  hgmapvv  38000  pellexlem5  38240  dfac11  38474  dfacbasgrp  38520  dgraalem  38557  dgraaub  38560  aaitgo  38574  sdrgacs  38613  cntzsdrg  38614  proot1ex  38621  isdomn3  38624  deg1mhm  38627  ofdivrec  39364  ofdivcan4  39365  ofdivdiv2  39366  expgrowth  39373  binomcxplemnotnn0  39394  dvdivbd  40932  dvdivcncf  40936  dirkeritg  41112  fourierdlem39  41156  fourierdlem57  41173  fourierdlem58  41174  fourierdlem59  41175  fourierdlem68  41184  fourierdlem76  41192  fourierdlem103  41219  fourierdlem104  41220  fourierdlem111  41227  setsnidel  42234  odz2prm2pw  42304  fmtnoprmfac1  42306  fmtnoprmfac2  42308  sfprmdvdsmersenne  42349  lighneallem2  42352  lighneallem3  42353  lighneal  42357  oddprmALTV  42427  evenprm2  42452  oddprmne2  42453  odd2prm2  42456  even3prm2  42457  sprvalpwn0  42579  2zrngnmrid  42796  fdmdifeqresdif  42966  lincext1  43089  lindslinindsimp2lem5  43097  rege1logbrege0  43198  fllogbd  43200  relogbmulbexp  43201  relogbdivb  43202  nnpw2blen  43220  blennngt2o2  43232  blennn0e2  43234  dignn0ldlem  43242  line  43282  rrxline  43284  aacllem  43442