MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldifsn Structured version   Visualization version   GIF version

Theorem eldifsn 4713
Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
Assertion
Ref Expression
eldifsn (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))

Proof of Theorem eldifsn
StepHypRef Expression
1 eldif 3945 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2 elsng 4573 . . . 4 (𝐴𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
32necon3bbid 3053 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴𝐶))
43pm5.32i 575 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
51, 4bitri 276 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396  wcel 2105  wne 3016  cdif 3932  {csn 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-v 3497  df-dif 3938  df-sn 4560
This theorem is referenced by:  elpwdifsn  4715  eldifsni  4716  rexdifsn  4721  raldifsni  4722  eldifvsn  4724  difsn  4725  prproe  4830  sossfld  6037  tpres  6956  onmindif2  7515  mptsuppd  7844  suppssr  7852  suppssov1  7853  suppsssn  7856  suppssfv  7857  dif1o  8116  difsnen  8588  limenpsi  8681  frfi  8752  fofinf1o  8788  en2eleq  9423  en2other2  9424  dfac8clem  9447  acni2  9461  acndom  9466  acnnum  9467  dfac9  9551  dfacacn  9556  kmlem3  9567  kmlem4  9568  fin23lem21  9750  canthp1lem2  10064  elni  10287  mulnzcnopr  11275  divval  11289  elnnne0  11900  elq  12339  rpcndif0  12398  modfzo0difsn  13301  modsumfzodifsn  13302  expcl2lem  13431  expclzlem  13443  hashdifpr  13766  hashgt23el  13775  prprrab  13821  hashle2prv  13826  reccn2  14943  rlimdiv  14992  eff2  15442  tanval  15471  rpnnen2lem9  15565  fzo0dvdseq  15663  oddprmgt2  16033  oddprmdvds  16229  4sqlem19  16289  prmlem0  16429  prmlem1a  16430  setsnid  16529  grpinvnzcl  18111  symgextf  18476  f1omvdmvd  18502  pmtrprfv  18512  odcau  18660  efgsf  18786  efgsrel  18791  efgs1  18792  efgs1b  18793  efgsp1  18794  efgsres  18795  efgredlema  18797  efgredlemd  18801  efgrelexlemb  18807  gsumpt  19013  dmdprdd  19052  dprdcntz  19061  dprdfeq0  19075  dprd2da  19095  drngunit  19438  isdrng2  19443  drngid2  19449  isdrngd  19458  issubdrg  19491  sdrgacs  19511  cntzsdrg  19512  abvtriv  19543  islss  19637  lssneln0  19655  lssssr  19656  lbsind  19783  lbspss  19785  lspabs3  19824  lspsneq  19825  lspfixed  19831  lspexch  19832  islbs2  19857  isdomn2  20002  domnrrg  20003  mvrcl  20159  coe1tmmul2  20374  cnflddiv  20505  cnfldinv  20506  xrs1mnd  20513  xrs10  20514  xrge0subm  20516  cnsubdrglem  20526  cnmgpid  20537  cnmsubglem  20538  gzrngunit  20541  zringunit  20565  zringndrg  20567  domnchr  20609  cnmsgngrp  20653  psgninv  20656  psgndiflemB  20674  lindfind  20890  lindsind  20891  lindff1  20894  lindfrn  20895  mdetunilem9  21159  maducoeval2  21179  gsummatr01lem4  21197  ist1-2  21885  cmpfi  21946  2ndcdisj  21994  2ndcsep  21997  locfincmp  22064  alexsublem  22582  cldsubg  22648  imasdsf1olem  22912  prdsxmslem2  23068  reperflem  23355  xrge0gsumle  23370  xrge0tsms  23371  divcn  23405  evth  23492  cvsdiv  23665  cvsdivcl  23666  cphreccllem  23711  bcthlem5  23860  itg11  24221  i1fmullem  24224  i1fadd  24225  itg1addlem2  24227  i1fmulc  24233  itg1mulc  24234  ellimc3  24406  limcmpt2  24411  dvlem  24423  dvidlem  24442  dvcnp  24445  dvcobr  24472  dvrec  24481  dvrecg  24499  dvmptdiv  24500  dvcnvlem  24502  dvexp3  24504  dveflem  24505  dvferm1lem  24510  dvferm2lem  24512  lhop1lem  24539  ftc1lem5  24566  mdegleb  24587  coe1mul3  24622  ply1nz  24644  fta1blem  24691  fta1b  24692  ig1peu  24694  ig1pdvds  24699  plyeq0lem  24729  dgrub  24753  quotval  24810  fta1lem  24825  fta1  24826  elqaalem3  24839  qaa  24841  iaa  24843  aareccl  24844  aannenlem2  24847  abelthlem8  24956  abelth  24958  eff1olem  25059  logrncl  25078  eflog  25087  logeftb  25094  logdmss  25152  dvlog  25161  logbcl  25272  logbid1  25273  logb1  25274  elogb  25275  logbchbase  25276  relogbval  25277  relogbcl  25278  relogbreexp  25280  relogbmul  25282  nnlogbexp  25286  relogbcxp  25290  cxplogb  25291  relogbcxpb  25292  logbf  25294  logblog  25297  2logb9irrALT  25303  sqrt2cxp2logb9e3  25304  angval  25306  dcubic  25351  rlimcnp  25471  efrlim  25475  logexprlim  25729  dchrghm  25760  dchrabs  25764  lgsfcl2  25807  lgsval2lem  25811  lgsval3  25819  lgsmod  25827  lgsdirprm  25835  lgsne0  25839  gausslemma2dlem0f  25865  lgsquad2lem2  25889  2lgsoddprm  25920  2sqlem11  25933  2sqblem  25935  dchrvmaeq0  26008  rpvmasum2  26016  dchrisum0re  26017  qrngdiv  26128  tglngval  26265  tgisline  26341  axlowdimlem9  26664  axlowdimlem12  26667  axlowdimlem13  26668  elntg2  26699  upgrbi  26806  upgr1elem  26825  umgrislfupgrlem  26835  edgupgr  26847  subgruhgredgd  26994  upgrreslem  27014  nbgrel  27050  nbupgr  27054  nbupgrel  27055  nbumgrvtx  27056  nbgrssovtx  27071  nbupgrres  27074  nbusgrvtxm1uvtx  27115  nbupgruvtxres  27117  iscplgredg  27127  cusgredg  27134  cusgrfilem2  27166  usgredgsscusgredg  27169  1loopgrnb0  27212  1egrvtxdg0  27221  uhgrvd00  27244  vtxdginducedm1lem4  27252  eupth2lem3lem3  27937  frcond1  27973  frcond4  27977  2pthfrgr  27991  3cyclfrgrrn1  27992  n4cyclfrgr  27998  frgrwopreglem4a  28017  numclwwlk5  28095  suppss3  30387  xdivval  30523  xrge0tsmsd  30620  pmtrcnel  30661  pmtrcnelor  30663  0nellinds  30863  extdg1id  30953  submatminr1  30975  ordtconnlem1  31067  ispisys2  31312  sigapisys  31314  sibfinima  31497  sseqf  31550  signswch  31731  signstfvn  31739  signsvtn0  31740  signstfvneq0  31742  signstfvcl  31743  signstfveq0a  31746  signstfveq0  31747  signsvfn  31752  signsvtp  31753  signsvtn  31754  signsvfpn  31755  signsvfnn  31756  signlem0  31757  bnj158  31899  bnj168  31900  bnj529  31912  bnj906  32102  bnj970  32119  exdifsn  32243  cusgredgex2  32267  subfacp1lem5  32329  cvmsi  32410  cvmsval  32411  cvmsdisj  32415  cvmscld  32418  cvmsss2  32419  satfv1lem  32507  sinccvglem  32813  circum  32815  unbdqndv2lem2  33747  bj-0int  34288  lindsadd  34767  lindsenlbs  34769  matunitlindflem2  34771  matunitlindf  34772  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem16  34790  poimirlem18  34792  poimirlem19  34793  poimirlem21  34795  poimirlem22  34796  poimirlem24  34798  poimirlem25  34799  poimirlem26  34800  poimirlem27  34801  itg2addnclem2  34826  sdclem1  34901  rrncmslem  34993  rrnequiv  34996  isdrngo2  35119  isdrngo3  35120  prtlem100  35877  prter2  35899  prter3  35900  lsatlspsn2  36010  lsateln0  36013  lsatn0  36017  lsatspn0  36018  lsatcmp  36021  lsatelbN  36024  islshpat  36035  lsat0cv  36051  lkrlspeqN  36189  dvheveccl  38130  dihlatat  38355  dochnel  38411  dihjat1  38447  dvh4dimlem  38461  dochsnkr2cl  38492  dochkr1  38496  dochkr1OLDN  38497  lcfl6lem  38516  lcfl9a  38523  lclkrlem2l  38536  lclkrlem2o  38539  lclkrlem2q  38541  lcfrlem9  38568  lcfrlem16  38576  lcfrlem17  38577  lcfrlem27  38587  lcfrlem37  38597  lcfrlem38  38598  lcfrlem40  38600  lcdlkreqN  38640  mapdrvallem2  38663  mapdn0  38687  mapdpglem20  38709  mapdpglem30  38720  mapdindp0  38737  mapdhcl  38745  mapdh6aN  38753  mapdh6dN  38757  mapdh6eN  38758  mapdh6kN  38764  mapdh8  38806  hdmap1l6a  38827  hdmap1l6d  38831  hdmap1l6e  38832  hdmap1l6k  38838  hdmapval3N  38856  hdmap10  38858  hdmap11lem2  38860  hdmapnzcl  38863  hdmaprnlem3eN  38876  hdmaprnlem17N  38881  hdmap14lem4a  38889  hdmap14lem7  38892  hdmap14lem14  38899  hgmaprnlem5N  38918  hdmaplkr  38931  hdmapip0  38933  hgmapvvlem2  38942  hgmapvvlem3  38943  hgmapvv  38944  0prjspnlem  39148  pellexlem5  39310  dfac11  39542  dfacbasgrp  39588  dgraalem  39625  dgraaub  39628  aaitgo  39642  proot1ex  39681  isdomn3  39684  deg1mhm  39687  ofdivrec  40538  ofdivcan4  40539  ofdivdiv2  40540  expgrowth  40547  binomcxplemnotnn0  40568  dvdivbd  42088  dvdivcncf  42092  dirkeritg  42268  fourierdlem39  42312  fourierdlem57  42329  fourierdlem58  42330  fourierdlem59  42331  fourierdlem68  42340  fourierdlem76  42348  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  setsnidel  43418  sprvalpwn0  43492  odz2prm2pw  43572  fmtnoprmfac1  43574  fmtnoprmfac2  43576  sfprmdvdsmersenne  43615  lighneallem2  43618  lighneallem3  43619  lighneal  43623  oddprmALTV  43699  evenprm2  43726  oddprmne2  43727  odd2prm2  43730  even3prm2  43731  2zrngnmrid  44119  lincext1  44407  lindslinindsimp2lem5  44415  rege1logbrege0  44516  fllogbd  44518  relogbmulbexp  44519  relogbdivb  44520  nnpw2blen  44538  blennngt2o2  44550  blennn0e2  44552  dignn0ldlem  44560  line  44617  rrxline  44619  aacllem  44800
  Copyright terms: Public domain W3C validator