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

Theorem eldifsn 4125
Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
Assertion
Ref Expression
eldifsn  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )

Proof of Theorem eldifsn
StepHypRef Expression
1 eldif 3446 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 4021 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2667 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C } 
<->  A  =/=  C ) )
43pm5.32i 641 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
51, 4bitri 252 1  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187    /\ wa 370    e. wcel 1872    =/= wne 2614    \ cdif 3433   {csn 3998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-v 3082  df-dif 3439  df-sn 3999
This theorem is referenced by:  eldifsni  4126  rexdifsn  4129  raldifsni  4130  eldifvsn  4132  difsn  4134  sossfld  5302  tpres  6132  mpt2difsnif  6403  onmindif2  6653  mptsuppd  6949  suppssr  6957  suppssov1  6958  suppsssn  6961  suppssfv  6962  dif1o  7213  difsnen  7663  limenpsi  7756  frfi  7825  fofinf1o  7861  wemapso2lem  8076  en2eleq  8447  en2other2  8448  dfac8clem  8470  acni2  8484  acndom  8489  acnnum  8490  dfac9  8573  dfacacn  8578  kmlem3  8589  kmlem4  8590  fin23lem21  8776  canthp1lem2  9085  elni  9308  mulnzcnopr  10265  divval  10279  elnnne0  10890  elq  11273  rpcndif0  11327  expcl2lem  12290  expclzlem  12302  reccn2  13659  rlimdiv  13708  eff2  14152  tanval  14181  rpnnen2lem9  14274  fzo0dvdseq  14357  4sqlem19  14912  prmlem0  15076  prmlem1a  15077  setsnid  15164  grpinvnzcl  16725  symgextf  17057  symgextfv  17058  f1omvdmvd  17083  pmtrprfv  17093  odcau  17255  efgsf  17378  efgsrel  17383  efgs1  17384  efgs1b  17385  efgsp1  17386  efgsres  17387  efgredlema  17389  efgredlemd  17393  efgrelexlemb  17399  gsumpt  17593  dmdprdd  17630  dprdcntz  17639  dprdfeq0  17654  dprd2da  17674  drngunit  17979  isdrng2  17984  drngid2  17990  isdrngd  17999  issubdrg  18032  abvtriv  18068  islss  18157  lssneln0  18174  lssssr  18175  lbsind  18302  lbspss  18304  lspabs3  18343  lspsneq  18344  lspfixed  18350  lspexch  18351  islbs2  18376  isdomn2  18522  domnrrg  18523  mvrcl  18672  coe1tmmul2  18868  cnflddiv  18997  cnfldinv  18998  xrs1mnd  19005  xrs10  19006  xrge0subm  19008  cnsubdrglem  19018  cnmsubglem  19029  gzrngunit  19032  zringunit  19060  domnchr  19101  cnmsgngrp  19145  psgninv  19148  psgndiflemB  19166  lindfind  19372  lindsind  19373  lindff1  19376  lindfrn  19377  mdetunilem9  19643  maducoeval2  19663  gsummatr01lem4  19681  ist1-2  20361  cmpfi  20421  2ndcdisj  20469  2ndcsep  20472  locfincmp  20539  alexsublem  21057  cldsubg  21123  imasdsf1olem  21386  prdsxmslem2  21542  reperflem  21834  xrge0gsumle  21849  xrge0tsms  21850  divcn  21898  evth  21985  cvsdiv  22138  cvsdivcl  22139  cphreccllem  22154  bcthlem5  22294  itg11  22647  i1fmullem  22650  i1fadd  22651  itg1addlem2  22653  i1fmulc  22659  itg1mulc  22660  ellimc3  22832  limcmpt2  22837  dvlem  22849  dvidlem  22868  dvcnp  22871  dvcobr  22898  dvrec  22907  dvcnvlem  22926  dvexp3  22928  dveflem  22929  dvferm1lem  22934  dvferm2lem  22936  lhop1lem  22963  ftc1lem5  22990  mdegleb  23011  coe1mul3  23046  ply1nz  23068  fta1blem  23117  fta1b  23118  ig1peu  23120  ig1peuOLD  23121  ig1pdvds  23126  ig1pdvdsOLD  23132  plyeq0lem  23162  dgrub  23186  quotval  23243  fta1lem  23258  fta1  23259  elqaalem3  23272  elqaalem3OLD  23275  qaa  23277  iaa  23279  aareccl  23280  aannenlem2  23283  abelthlem8  23392  abelth  23394  reefgim  23403  eff1olem  23495  logrncl  23515  eflog  23524  logeftb  23531  logdmss  23585  dvlog  23594  logbcl  23702  logbid1  23703  logb1  23704  elogb  23705  logbchbase  23706  relogbval  23707  relogbcl  23708  relogbreexp  23710  relogbmul  23712  nnlogbexp  23716  relogbcxp  23720  cxplogb  23721  relogbcxpb  23722  logbf  23724  logblog  23727  angval  23728  dcubic  23770  rlimcnp  23889  efrlim  23893  logexprlim  24151  dchrghm  24182  dchrabs  24186  lgsfcl2  24228  lgsval2lem  24232  lgsval3  24240  lgsmod  24247  lgsdirprm  24255  lgsne0  24259  lgsquad2lem2  24285  2sqlem11  24301  2sqblem  24303  dchrvmaeq0  24340  rpvmasum2  24348  dchrisum0re  24349  qrngdiv  24460  tglngval  24594  tgisline  24670  axlowdimlem9  24978  axlowdimlem12  24981  axlowdimlem13  24982  umgra1  25051  uslgra1  25097  cusgrarn  25185  cusgrafilem2  25206  sizeusglecusglem1  25210  nbhashuvtx  25642  umgrabi  25709  2pthfrgra  25737  3cyclfrgrarn1  25738  n4cyclfrgra  25744  ablomul  26081  mulid  26082  suppss3  28318  xdivval  28395  xrge0tsmsd  28556  submatminr1  28644  ordtconlem1  28738  ispisys2  28983  sigapisys  28985  sibfinima  29180  sseqf  29233  signswch  29458  signstfvn  29466  signsvtn0  29467  signstfvcl  29470  signstfveq0a  29473  signstfveq0  29474  signsvfn  29479  signsvtp  29480  signsvtn  29481  signsvfpn  29482  signsvfnn  29483  signlem0  29484  bnj158  29545  bnj168  29546  bnj529  29559  bnj906  29749  bnj970  29766  subfacp1lem5  29915  cvmsi  29996  cvmsval  29997  cvmsdisj  30001  cvmscld  30004  cvmsss2  30005  sinccvglem  30324  circum  30326  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem16  31920  poimirlem18  31922  poimirlem19  31923  poimirlem21  31925  poimirlem22  31926  poimirlem24  31928  poimirlem25  31929  poimirlem26  31930  poimirlem27  31931  itg2addnclem2  31958  sdclem1  32036  rrncmslem  32128  rrnequiv  32131  isdrngo2  32161  isdrngo3  32162  prtlem100  32395  prter2  32421  prter3  32422  lsatlspsn2  32527  lsateln0  32530  lsatn0  32534  lsatspn0  32535  lsatcmp  32538  lsatelbN  32541  islshpat  32552  lsat0cv  32568  lkrlspeqN  32706  dvheveccl  34649  dihlatat  34874  dochnel  34930  dihjat1  34966  dvh4dimlem  34980  dochsnkr2cl  35011  dochkr1  35015  dochkr1OLDN  35016  lcfl6lem  35035  lcfl9a  35042  lclkrlem2l  35055  lclkrlem2o  35058  lclkrlem2q  35060  lcfrlem9  35087  lcfrlem16  35095  lcfrlem17  35096  lcfrlem27  35106  lcfrlem37  35116  lcfrlem38  35117  lcfrlem40  35119  lcdlkreqN  35159  mapdrvallem2  35182  mapdn0  35206  mapdpglem20  35228  mapdpglem30  35239  mapdindp0  35256  mapdhcl  35264  mapdh6aN  35272  mapdh6dN  35276  mapdh6eN  35277  mapdh6kN  35283  mapdh8  35326  hdmap1l6a  35347  hdmap1l6d  35351  hdmap1l6e  35352  hdmap1l6k  35358  hdmapval3N  35378  hdmap10  35380  hdmap11lem2  35382  hdmapnzcl  35385  hdmaprnlem3eN  35398  hdmaprnlem17N  35403  hdmap14lem4a  35411  hdmap14lem7  35414  hdmap14lem14  35421  hgmaprnlem5N  35440  hdmaplkr  35453  hdmapip0  35455  hgmapvvlem2  35464  hgmapvvlem3  35465  hgmapvv  35466  pellexlem5  35647  dfac11  35890  dfacbasgrp  35937  dgraalem  35977  dgraalemOLD  35978  dgraaub  35983  dgraaubOLD  35984  aaitgo  35998  sdrgacs  36037  cntzsdrg  36038  proot1ex  36048  isdomn3  36051  deg1mhm  36054  ofdivrec  36645  ofdivcan4  36646  ofdivdiv2  36647  expgrowth  36654  binomcxplemnotnn0  36675  dvrecg  37722  dvmptdiv  37729  dvdivbd  37735  dvdivcncf  37739  dirkeritg  37904  fourierdlem39  37949  fourierdlem57  37967  fourierdlem58  37968  fourierdlem59  37969  fourierdlem68  37978  fourierdlem76  37986  fourierdlem103  38013  fourierdlem104  38014  fourierdlem111  38021  oddprmALTV  38686  evenprm2  38712  elpwdifsn  38856  umgr1lem  39014  edgumgra  39043  umgredg  39078  subgruhgredgd  39130  nbgrel  39177  nbumgr  39179  nbumgrel  39180  nbusgrvtx  39181  nbgrssovtx  39197  nbumgrres  39203  nbumgruvtxres  39237  iscplgredg  39242  cusgredg  39249  cusgrexi  39264  cusgrfilem2  39274  usgredgsscusgredg  39277  2zrngnmrid  39570  fdmdifeqresdif  39745  lincext1  39869  lindslinindsimp2lem5  39877  rege1logbrege0  39991  fllogbd  39993  relogbmulbexp  39994  relogbdivb  39995  nnpw2blen  40013  blennngt2o2  40025  blennn0e2  40027  dignn0ldlem  40035  aacllem  40162
  Copyright terms: Public domain W3C validator