Theorem eldifsn 4786

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   ≠ wne 2940   ∖ cdif 3948  {csn 4626

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-sn 4627

This theorem is referenced by:  eldifsnd  4787  elpwdifsn  4789  eldifsni  4790  rexdifsn  4794  raldifsni  4795  eldifvsn  4797  difsn  4798  sossfld  6206  tpres  7221  onmindif2  7827  xpord3pred  8177  xpord3inddlem  8179  mptsuppd  8212  suppssr  8220  suppssov1  8222  suppssov2  8223  suppsssn  8226  suppssfv  8227  dif1o  8538  difsnen  9093  limenpsi  9192  frfi  9321  fofinf1o  9372  en2eleq  10048  en2other2  10049  dfac8clem  10072  acni2  10086  acndom  10091  acnnum  10092  dfac9  10177  dfacacn  10182  kmlem3  10193  kmlem4  10194  fin23lem21  10379  canthp1lem2  10693  elni  10916  mulnzcnf  11909  divval  11924  elnnne0  12540  elq  12992  rpcndif0  13054  modfzo0difsn  13984  modsumfzodifsn  13985  expcl2lem  14114  expclzlem  14124  hashdifpr  14454  hashgt23el  14463  prprrab  14512  hashle2prv  14517  reccn2  15633  rlimdiv  15682  eff2  16135  tanval  16164  rpnnen2lem9  16258  fzo0dvdseq  16360  oddprmgt2  16736  oddprmdvds  16941  4sqlem19  17001  prmlem0  17143  prmlem1a  17144  setsnid  17245  setsnidOLD  17246  grpinvnzcl  19029  symgextf  19435  f1omvdmvd  19461  pmtrprfv  19471  odcau  19622  efgsf  19747  efgsrel  19752  efgs1  19753  efgs1b  19754  efgsp1  19755  efgsres  19756  efgredlema  19758  efgredlemd  19762  efgrelexlemb  19768  gsumpt  19980  dmdprdd  20019  dprdcntz  20028  dprdfeq0  20042  dprd2da  20062  isdomn2OLD  20712  domnrrg  20713  isdomn3  20715  drngunit  20734  isdrng2  20743  drngmcl  20750  drngid2  20752  isdrngd  20765  isdrngdOLD  20767  issubdrg  20781  sdrgacs  20802  cntzsdrg  20803  islss  20932  lssneln0  20951  lssssr  20952  lbsind  21079  lbspss  21081  lspabs3  21123  lspsneq  21124  lspfixed  21130  lspexch  21131  islbs2  21156  cnflddivOLD  21414  cnfldinv  21415  xrs1mnd  21422  xrs10  21423  xrge0subm  21425  cnsubdrglem  21436  cnmgpid  21447  cnmsubglem  21448  gzrngunit  21451  zringunit  21477  zringndrg  21479  domnchr  21547  cnmsgngrp  21597  psgninv  21600  psgndiflemB  21618  lindfind  21836  lindsind  21837  lindff1  21840  lindfrn  21841  mvrcl  22012  coe1tmmul2  22279  mdetunilem9  22626  maducoeval2  22646  gsummatr01lem4  22664  ist1-2  23355  cmpfi  23416  2ndcdisj  23464  2ndcsep  23467  locfincmp  23534  alexsublem  24052  cldsubg  24119  imasdsf1olem  24383  prdsxmslem2  24542  reperflem  24840  xrge0gsumle  24855  xrge0tsms  24856  divcnOLD  24890  divcn  24892  evth  24991  cvsdiv  25165  cvsdivcl  25166  cphreccllem  25212  bcthlem5  25362  itg11  25726  i1fmullem  25729  i1fadd  25730  itg1addlem2  25732  i1fmulc  25738  itg1mulc  25739  ellimc3  25914  limcmpt2  25919  dvlem  25931  dvidlem  25950  dvcnp  25954  dvcobr  25983  dvcobrOLD  25984  dvrec  25993  dvrecg  26011  dvmptdiv  26012  dvcnvlem  26014  dvexp3  26016  dveflem  26017  dvferm1lem  26022  dvferm2lem  26024  lhop1lem  26052  ftc1lem5  26081  mdegleb  26103  coe1mul3  26138  ply1nz  26161  fta1blem  26210  fta1b  26211  ig1peu  26214  ig1pdvds  26219  plyeq0lem  26249  dgrub  26273  quotval  26334  fta1lem  26349  fta1  26350  elqaalem3  26363  qaa  26365  iaa  26367  aareccl  26368  aannenlem2  26371  abelthlem8  26483  abelth  26485  eff1olem  26590  logrncl  26609  eflog  26618  logeftb  26625  logdmss  26684  dvlog  26693  logbcl  26810  logbid1  26811  logb1  26812  elogb  26813  logbchbase  26814  relogbval  26815  relogbcl  26816  relogbreexp  26818  relogbmul  26820  nnlogbexp  26824  relogbcxp  26828  cxplogb  26829  relogbcxpb  26830  logbf  26832  logblog  26835  2logb9irrALT  26841  sqrt2cxp2logb9e3  26842  angval  26844  dcubic  26889  rlimcnp  27008  efrlim  27012  efrlimOLD  27013  logexprlim  27269  dchrghm  27300  dchrabs  27304  lgsfcl2  27347  lgsval2lem  27351  lgsval3  27359  lgsmod  27367  lgsdirprm  27375  lgsne0  27379  gausslemma2dlem0f  27405  lgsquad2lem2  27429  2lgsoddprm  27460  2sqlem11  27473  2sqblem  27475  dchrvmaeq0  27548  rpvmasum2  27556  dchrisum0re  27557  qrngdiv  27668  addsval  27995  divsval  28215  elnns  28343  1nns  28352  tglngval  28559  tgisline  28635  axlowdimlem9  28965  axlowdimlem12  28968  axlowdimlem13  28969  elntg2  29000  upgrbi  29110  upgr1elem  29129  umgrislfupgrlem  29139  edgupgr  29151  subgruhgredgd  29301  upgrreslem  29321  nbgrel  29357  nbupgr  29361  nbupgrel  29362  nbumgrvtx  29363  nbgrssovtx  29378  nbupgrres  29381  nbusgrvtxm1uvtx  29422  nbupgruvtxres  29424  iscplgredg  29434  cusgredg  29441  cusgrfilem2  29474  usgredgsscusgredg  29477  1loopgrnb0  29520  1egrvtxdg0  29529  uhgrvd00  29552  vtxdginducedm1lem4  29560  eupth2lem3lem3  30249  frcond1  30285  frcond4  30289  2pthfrgr  30303  3cyclfrgrrn1  30304  n4cyclfrgr  30310  frgrwopreglem4a  30329  numclwwlk5  30407  ressupprn  32699  suppss3  32735  xdivval  32901  xrge0tsmsd  33065  pmtrcnel  33109  pmtrcnelor  33111  0nellinds  33398  dvdsruasso  33413  mxidlirredi  33499  extdg1id  33716  irngnzply1  33741  submatminr1  33809  ordtconnlem1  33923  ispisys2  34154  sigapisys  34156  sibfinima  34341  sseqf  34394  signswch  34576  signstfvn  34584  signsvtn0  34585  signstfvneq0  34587  signstfvcl  34588  signstfveq0a  34591  signstfveq0  34592  signsvfn  34597  signsvtp  34598  signsvtn  34599  signsvfpn  34600  signsvfnn  34601  signlem0  34602  bnj158  34743  bnj168  34744  bnj529  34755  bnj906  34944  bnj970  34961  exdifsn  35093  cusgredgex2  35128  subfacp1lem5  35189  cvmsi  35270  cvmsval  35271  cvmsdisj  35275  cvmscld  35278  cvmsss2  35279  satfv1lem  35367  sinccvglem  35677  circum  35679  mpomulnzcnf  36300  unbdqndv2lem2  36511  bj-0int  37102  lindsadd  37620  lindsenlbs  37622  matunitlindflem2  37624  matunitlindf  37625  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem16  37643  poimirlem18  37645  poimirlem19  37646  poimirlem21  37648  poimirlem22  37649  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  itg2addnclem2  37679  sdclem1  37750  rrncmslem  37839  rrnequiv  37842  isdrngo2  37965  isdrngo3  37966  prtlem100  38860  prter2  38882  prter3  38883  lsatlspsn2  38993  lsateln0  38996  lsatn0  39000  lsatspn0  39001  lsatcmp  39004  lsatelbN  39007  islshpat  39018  lsat0cv  39034  lkrlspeqN  39172  dvheveccl  41114  dihlatat  41339  dochnel  41395  dihjat1  41431  dvh4dimlem  41445  dochsnkr2cl  41476  dochkr1  41480  dochkr1OLDN  41481  lcfl6lem  41500  lcfl9a  41507  lclkrlem2l  41520  lclkrlem2o  41523  lclkrlem2q  41525  lcfrlem9  41552  lcfrlem16  41560  lcfrlem17  41561  lcfrlem27  41571  lcfrlem37  41581  lcfrlem38  41582  lcfrlem40  41584  lcdlkreqN  41624  mapdrvallem2  41647  mapdn0  41671  mapdpglem20  41693  mapdpglem30  41704  mapdindp0  41721  mapdhcl  41729  mapdh6aN  41737  mapdh6dN  41741  mapdh6eN  41742  mapdh6kN  41748  mapdh8  41790  hdmap1l6a  41811  hdmap1l6d  41815  hdmap1l6e  41816  hdmap1l6k  41822  hdmapval3N  41840  hdmap10  41842  hdmap11lem2  41844  hdmapnzcl  41847  hdmaprnlem3eN  41860  hdmaprnlem17N  41865  hdmap14lem4a  41873  hdmap14lem7  41876  hdmap14lem14  41883  hgmaprnlem5N  41902  hdmaplkr  41915  hdmapip0  41917  hgmapvvlem2  41926  hgmapvvlem3  41927  hgmapvv  41928  redvmptabs  42390  readvrec2  42391  readvrec  42392  fiabv  42546  fsuppind  42600  0prjspnlem  42633  pellexlem5  42844  dfac11  43074  dfacbasgrp  43120  dgraalem  43157  dgraaub  43160  aaitgo  43174  proot1ex  43208  deg1mhm  43212  ofdivrec  44345  ofdivcan4  44346  ofdivdiv2  44347  expgrowth  44354  binomcxplemnotnn0  44375  dvdivbd  45938  dvdivcncf  45942  dirkeritg  46117  fourierdlem39  46161  fourierdlem57  46178  fourierdlem58  46179  fourierdlem59  46180  fourierdlem68  46189  fourierdlem76  46197  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  setsnidel  47364  sprvalpwn0  47470  odz2prm2pw  47550  fmtnoprmfac1  47552  fmtnoprmfac2  47554  sfprmdvdsmersenne  47590  lighneallem2  47593  lighneallem3  47594  lighneal  47598  oddprmALTV  47674  evenprm2  47701  oddprmne2  47702  odd2prm2  47705  even3prm2  47706  isubgruhgr  47854  grimuhgr  47878  2zrngnmrid  48172  lincext1  48371  lindslinindsimp2lem5  48379  rege1logbrege0  48479  fllogbd  48481  relogbmulbexp  48482  relogbdivb  48483  nnpw2blen  48501  blennngt2o2  48513  blennn0e2  48515  dignn0ldlem  48523  line  48653  rrxline  48655  aacllem  49320