Theorem eldifsn 4746

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 4599	. . . 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 3908  {csn 4585

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 3446  df-dif 3914  df-sn 4586

This theorem is referenced by:  eldifsnd  4747  elpwdifsn  4749  eldifsni  4750  rexdifsn  4754  raldifsni  4755  eldifvsn  4757  difsn  4758  sossfld  6148  tpres  7158  onmindif2  7764  xpord3pred  8109  xpord3inddlem  8111  mptsuppd  8144  suppssr  8152  suppssov1  8154  suppssov2  8155  suppsssn  8158  suppssfv  8159  dif1o  8442  difsnen  9001  limenpsi  9094  frfi  9209  fofinf1o  9260  en2eleq  9940  en2other2  9941  dfac8clem  9964  acni2  9978  acndom  9983  acnnum  9984  dfac9  10069  dfacacn  10074  kmlem3  10085  kmlem4  10086  fin23lem21  10271  canthp1lem2  10585  elni  10808  mulnzcnf  11803  divval  11818  elnnne0  12435  elq  12888  rpcndif0  12951  modfzo0difsn  13887  modsumfzodifsn  13888  expcl2lem  14017  expclzlem  14027  hashdifpr  14359  hashgt23el  14368  prprrab  14417  hashle2prv  14422  reccn2  15541  rlimdiv  15590  eff2  16045  tanval  16074  rpnnen2lem9  16168  fzo0dvdseq  16271  oddprmgt2  16647  oddprmdvds  16852  4sqlem19  16912  prmlem0  17054  prmlem1a  17055  setsnid  17156  grpinvnzcl  18927  symgextf  19333  f1omvdmvd  19359  pmtrprfv  19369  odcau  19520  efgsf  19645  efgsrel  19650  efgs1  19651  efgs1b  19652  efgsp1  19653  efgsres  19654  efgredlema  19656  efgredlemd  19660  efgrelexlemb  19666  gsumpt  19878  dmdprdd  19917  dprdcntz  19926  dprdfeq0  19940  dprd2da  19960  isdomn2OLD  20634  domnrrg  20635  isdomn3  20637  drngunit  20656  isdrng2  20665  drngmcl  20672  drngid2  20674  isdrngd  20687  isdrngdOLD  20689  issubdrg  20702  sdrgacs  20723  cntzsdrg  20724  islss  20874  lssneln0  20893  lssssr  20894  lbsind  21021  lbspss  21023  lspabs3  21065  lspsneq  21066  lspfixed  21072  lspexch  21073  islbs2  21098  cnflddivOLD  21345  cnfldinv  21346  cnsubdrglem  21362  cnmgpid  21373  cnmsubglem  21374  gzrngunit  21377  xrs1mnd  21384  xrs10  21385  xrge0subm  21387  zringunit  21410  zringndrg  21412  domnchr  21476  cnmsgngrp  21523  psgninv  21526  psgndiflemB  21544  lindfind  21760  lindsind  21761  lindff1  21764  lindfrn  21765  mvrcl  21936  coe1tmmul2  22197  mdetunilem9  22542  maducoeval2  22562  gsummatr01lem4  22580  ist1-2  23269  cmpfi  23330  2ndcdisj  23378  2ndcsep  23381  locfincmp  23448  alexsublem  23966  cldsubg  24033  imasdsf1olem  24296  prdsxmslem2  24452  reperflem  24742  xrge0gsumle  24757  xrge0tsms  24758  divcnOLD  24792  divcn  24794  evth  24893  cvsdiv  25067  cvsdivcl  25068  cphreccllem  25113  bcthlem5  25263  itg11  25627  i1fmullem  25630  i1fadd  25631  itg1addlem2  25633  i1fmulc  25639  itg1mulc  25640  ellimc3  25815  limcmpt2  25820  dvlem  25832  dvidlem  25851  dvcnp  25855  dvcobr  25884  dvcobrOLD  25885  dvrec  25894  dvrecg  25912  dvmptdiv  25913  dvcnvlem  25915  dvexp3  25917  dveflem  25918  dvferm1lem  25923  dvferm2lem  25925  lhop1lem  25953  ftc1lem5  25982  mdegleb  26004  coe1mul3  26039  ply1nz  26062  fta1blem  26111  fta1b  26112  ig1peu  26115  ig1pdvds  26120  plyeq0lem  26150  dgrub  26174  quotval  26235  fta1lem  26250  fta1  26251  elqaalem3  26264  qaa  26266  iaa  26268  aareccl  26269  aannenlem2  26272  abelthlem8  26384  abelth  26386  eff1olem  26492  logrncl  26511  eflog  26520  logeftb  26527  logdmss  26586  dvlog  26595  logbcl  26712  logbid1  26713  logb1  26714  elogb  26715  logbchbase  26716  relogbval  26717  relogbcl  26718  relogbreexp  26720  relogbmul  26722  nnlogbexp  26726  relogbcxp  26730  cxplogb  26731  relogbcxpb  26732  logbf  26734  logblog  26737  2logb9irrALT  26743  sqrt2cxp2logb9e3  26744  angval  26746  dcubic  26791  rlimcnp  26910  efrlim  26914  efrlimOLD  26915  logexprlim  27171  dchrghm  27202  dchrabs  27206  lgsfcl2  27249  lgsval2lem  27253  lgsval3  27261  lgsmod  27269  lgsdirprm  27277  lgsne0  27281  gausslemma2dlem0f  27307  lgsquad2lem2  27331  2lgsoddprm  27362  2sqlem11  27375  2sqblem  27377  dchrvmaeq0  27450  rpvmasum2  27458  dchrisum0re  27459  qrngdiv  27570  addsval  27911  divsval  28134  elnns  28274  1nns  28283  tglngval  28533  tgisline  28609  axlowdimlem9  28932  axlowdimlem12  28935  axlowdimlem13  28936  elntg2  28967  upgrbi  29075  upgr1elem  29094  umgrislfupgrlem  29104  edgupgr  29116  subgruhgredgd  29266  upgrreslem  29286  nbgrel  29322  nbupgr  29326  nbupgrel  29327  nbumgrvtx  29328  nbgrssovtx  29343  nbupgrres  29346  nbusgrvtxm1uvtx  29387  nbupgruvtxres  29389  iscplgredg  29399  cusgredg  29406  cusgrfilem2  29439  usgredgsscusgredg  29442  1loopgrnb0  29485  1egrvtxdg0  29494  uhgrvd00  29517  vtxdginducedm1lem4  29525  eupth2lem3lem3  30211  frcond1  30247  frcond4  30251  2pthfrgr  30265  3cyclfrgrrn1  30266  n4cyclfrgr  30272  frgrwopreglem4a  30291  numclwwlk5  30369  ressupprn  32665  suppss3  32699  xdivval  32891  xrge0tsmsd  33047  pmtrcnel  33063  pmtrcnelor  33065  0nellinds  33336  dvdsruasso  33351  mxidlirredi  33437  extdg1id  33656  irngnzply1  33681  submatminr1  33795  ordtconnlem1  33909  ispisys2  34138  sigapisys  34140  sibfinima  34325  sseqf  34378  signswch  34547  signstfvn  34555  signsvtn0  34556  signstfvneq0  34558  signstfvcl  34559  signstfveq0a  34562  signstfveq0  34563  signsvfn  34568  signsvtp  34569  signsvtn  34570  signsvfpn  34571  signsvfnn  34572  signlem0  34573  bnj158  34714  bnj168  34715  bnj529  34726  bnj906  34915  bnj970  34932  exdifsn  35064  cusgredgex2  35105  subfacp1lem5  35166  cvmsi  35247  cvmsval  35248  cvmsdisj  35252  cvmscld  35255  cvmsss2  35256  satfv1lem  35344  sinccvglem  35654  circum  35656  mpomulnzcnf  36282  unbdqndv2lem2  36493  bj-0int  37084  lindsadd  37602  lindsenlbs  37604  matunitlindflem2  37606  matunitlindf  37607  poimirlem6  37615  poimirlem7  37616  poimirlem8  37617  poimirlem16  37625  poimirlem18  37627  poimirlem19  37628  poimirlem21  37630  poimirlem22  37631  poimirlem24  37633  poimirlem25  37634  poimirlem26  37635  poimirlem27  37636  itg2addnclem2  37661  sdclem1  37732  rrncmslem  37821  rrnequiv  37824  isdrngo2  37947  isdrngo3  37948  eldmxrncnvepres  38391  eldmxrncnvepres2  38392  prtlem100  38847  prter2  38869  prter3  38870  lsatlspsn2  38980  lsateln0  38983  lsatn0  38987  lsatspn0  38988  lsatcmp  38991  lsatelbN  38994  islshpat  39005  lsat0cv  39021  lkrlspeqN  39159  dvheveccl  41101  dihlatat  41326  dochnel  41382  dihjat1  41418  dvh4dimlem  41432  dochsnkr2cl  41463  dochkr1  41467  dochkr1OLDN  41468  lcfl6lem  41487  lcfl9a  41494  lclkrlem2l  41507  lclkrlem2o  41510  lclkrlem2q  41512  lcfrlem9  41539  lcfrlem16  41547  lcfrlem17  41548  lcfrlem27  41558  lcfrlem37  41568  lcfrlem38  41569  lcfrlem40  41571  lcdlkreqN  41611  mapdrvallem2  41634  mapdn0  41658  mapdpglem20  41680  mapdpglem30  41691  mapdindp0  41708  mapdhcl  41716  mapdh6aN  41724  mapdh6dN  41728  mapdh6eN  41729  mapdh6kN  41735  mapdh8  41777  hdmap1l6a  41798  hdmap1l6d  41802  hdmap1l6e  41803  hdmap1l6k  41809  hdmapval3N  41827  hdmap10  41829  hdmap11lem2  41831  hdmapnzcl  41834  hdmaprnlem3eN  41847  hdmaprnlem17N  41852  hdmap14lem4a  41860  hdmap14lem7  41863  hdmap14lem14  41870  hgmaprnlem5N  41889  hdmaplkr  41902  hdmapip0  41904  hgmapvvlem2  41913  hgmapvvlem3  41914  hgmapvv  41915  redvmptabs  42343  readvrec2  42344  readvrec  42345  fiabv  42519  fsuppind  42573  0prjspnlem  42606  pellexlem5  42816  dfac11  43046  dfacbasgrp  43092  dgraalem  43129  dgraaub  43132  aaitgo  43146  proot1ex  43180  deg1mhm  43184  ofdivrec  44310  ofdivcan4  44311  ofdivdiv2  44312  expgrowth  44319  binomcxplemnotnn0  44340  dvdivbd  45916  dvdivcncf  45920  dirkeritg  46095  fourierdlem39  46139  fourierdlem57  46156  fourierdlem58  46157  fourierdlem59  46158  fourierdlem68  46167  fourierdlem76  46175  fourierdlem103  46202  fourierdlem104  46203  fourierdlem111  46210  setsnidel  47373  sprvalpwn0  47479  odz2prm2pw  47559  fmtnoprmfac1  47561  fmtnoprmfac2  47563  sfprmdvdsmersenne  47599  lighneallem2  47602  lighneallem3  47603  lighneal  47607  oddprmALTV  47683  evenprm2  47710  oddprmne2  47711  odd2prm2  47714  even3prm2  47715  isubgruhgr  47863  grimuhgr  47882  2zrngnmrid  48239  lincext1  48438  lindslinindsimp2lem5  48446  rege1logbrege0  48542  fllogbd  48544  relogbmulbexp  48545  relogbdivb  48546  nnpw2blen  48564  blennngt2o2  48576  blennn0e2  48578  dignn0ldlem  48586  line  48716  rrxline  48718  aacllem  49785