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

Theorem eldifsn 4128
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 3452 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 4025 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2678 . . 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 1870    =/= wne 2625    \ cdif 3439   {csn 4002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-v 3089  df-dif 3445  df-sn 4003
This theorem is referenced by:  eldifsni  4129  rexdifsn  4132  raldifsni  4133  eldifvsn  4135  difsn  4137  sossfld  5303  tpres  6132  mpt2difsnif  6403  onmindif2  6653  mptsuppd  6949  suppssr  6957  suppssov1  6958  suppsssn  6961  suppssfv  6962  dif1o  7210  difsnen  7660  limenpsi  7753  frfi  7822  fofinf1o  7858  wemapso2lem  8067  en2eleq  8438  en2other2  8439  dfac8clem  8461  acni2  8475  acndom  8480  acnnum  8481  dfac9  8564  dfacacn  8569  kmlem3  8580  kmlem4  8581  fin23lem21  8767  canthp1lem2  9077  elni  9300  mulnzcnopr  10257  divval  10271  elnnne0  10883  elq  11266  rpcndif0  11320  expcl2lem  12281  expclzlem  12293  reccn2  13638  rlimdiv  13687  eff2  14131  tanval  14160  rpnnen2lem9  14253  fzo0dvdseq  14336  4sqlem19  14876  prmlem0  15040  prmlem1a  15041  setsnid  15128  grpinvnzcl  16677  symgextf  17009  symgextfv  17010  f1omvdmvd  17035  pmtrprfv  17045  odcau  17191  efgsf  17314  efgsrel  17319  efgs1  17320  efgs1b  17321  efgsp1  17322  efgsres  17323  efgredlema  17325  efgredlemd  17329  efgrelexlemb  17335  gsumpt  17529  dmdprdd  17566  dprdcntz  17575  dprdfeq0  17590  dprd2da  17610  drngunit  17915  isdrng2  17920  drngid2  17926  isdrngd  17935  issubdrg  17968  abvtriv  18004  islss  18093  lssneln0  18110  lssssr  18111  lbsind  18238  lbspss  18240  lspabs3  18279  lspsneq  18280  lspfixed  18286  lspexch  18287  islbs2  18312  isdomn2  18458  domnrrg  18459  mvrcl  18608  coe1tmmul2  18804  cnflddiv  18933  cnfldinv  18934  xrs1mnd  18941  xrs10  18942  xrge0subm  18944  cnsubdrglem  18954  cnmsubglem  18965  gzrngunit  18968  zringunit  18993  domnchr  19034  cnmsgngrp  19078  psgninv  19081  psgndiflemB  19099  lindfind  19305  lindsind  19306  lindff1  19309  lindfrn  19310  mdetunilem9  19576  maducoeval2  19596  gsummatr01lem4  19614  ist1-2  20294  cmpfi  20354  2ndcdisj  20402  2ndcsep  20405  locfincmp  20472  alexsublem  20990  cldsubg  21056  imasdsf1olem  21319  prdsxmslem2  21475  reperflem  21747  xrge0gsumle  21762  xrge0tsms  21763  divcn  21796  evth  21883  cvsdiv  22033  cvsdivcl  22034  cphreccllem  22049  bcthlem5  22189  itg11  22526  i1fmullem  22529  i1fadd  22530  itg1addlem2  22532  i1fmulc  22538  itg1mulc  22539  ellimc3  22711  limcmpt2  22716  dvlem  22728  dvidlem  22747  dvcnp  22750  dvcobr  22777  dvrec  22786  dvcnvlem  22805  dvexp3  22807  dveflem  22808  dvferm1lem  22813  dvferm2lem  22815  lhop1lem  22842  ftc1lem5  22869  mdegleb  22890  coe1mul3  22925  ply1nz  22947  fta1blem  22994  fta1b  22995  ig1peu  22997  ig1pdvds  23002  plyeq0lem  23032  dgrub  23056  quotval  23113  fta1lem  23128  fta1  23129  elqaalem3  23142  qaa  23144  iaa  23146  aareccl  23147  aannenlem2  23150  abelthlem8  23259  abelth  23261  reefgim  23270  eff1olem  23362  logrncl  23382  eflog  23391  logeftb  23398  logdmss  23452  dvlog  23461  logbcl  23569  logbid1  23570  logb1  23571  elogb  23572  logbchbase  23573  relogbval  23574  relogbcl  23575  relogbreexp  23577  relogbmul  23579  nnlogbexp  23583  relogbcxp  23587  cxplogb  23588  relogbcxpb  23589  logbf  23591  logblog  23594  angval  23595  dcubic  23637  rlimcnp  23756  efrlim  23760  logexprlim  24016  dchrghm  24047  dchrabs  24051  lgsfcl2  24093  lgsval2lem  24097  lgsval3  24105  lgsmod  24112  lgsdirprm  24120  lgsne0  24124  lgsquad2lem2  24150  2sqlem11  24166  2sqblem  24168  dchrvmaeq0  24205  rpvmasum2  24213  dchrisum0re  24214  qrngdiv  24325  tglngval  24456  tgisline  24531  axlowdimlem9  24826  axlowdimlem12  24829  axlowdimlem13  24830  umgra1  24899  uslgra1  24945  cusgrarn  25032  cusgrafilem2  25053  sizeusglecusglem1  25057  nbhashuvtx  25489  umgrabi  25556  2pthfrgra  25584  3cyclfrgrarn1  25585  n4cyclfrgra  25591  ablomul  25928  mulid  25929  suppss3  28155  xdivval  28226  xrge0tsmsd  28387  submatminr1  28475  ordtconlem1  28569  ispisys2  28814  sigapisys  28816  sibfinima  29000  sseqf  29051  signswch  29238  signstfvn  29246  signsvtn0  29247  signstfvcl  29250  signstfveq0a  29253  signstfveq0  29254  signsvfn  29259  signsvtp  29260  signsvtn  29261  signsvfpn  29262  signsvfnn  29263  signlem0  29264  bnj158  29325  bnj168  29326  bnj529  29339  bnj906  29529  bnj970  29546  subfacp1lem5  29695  cvmsi  29776  cvmsval  29777  cvmsdisj  29781  cvmscld  29784  cvmsss2  29785  sinccvglem  30104  circum  30106  poimirlem6  31649  poimirlem7  31650  poimirlem8  31651  poimirlem16  31659  poimirlem18  31661  poimirlem19  31662  poimirlem21  31664  poimirlem22  31665  poimirlem24  31667  poimirlem25  31668  poimirlem26  31669  poimirlem27  31670  itg2addnclem2  31697  sdclem1  31775  rrncmslem  31867  rrnequiv  31870  isdrngo2  31900  isdrngo3  31901  prtlem100  32134  prter2  32160  prter3  32161  lsatlspsn2  32266  lsateln0  32269  lsatn0  32273  lsatspn0  32274  lsatcmp  32277  lsatelbN  32280  islshpat  32291  lsat0cv  32307  lkrlspeqN  32445  dvheveccl  34388  dihlatat  34613  dochnel  34669  dihjat1  34705  dvh4dimlem  34719  dochsnkr2cl  34750  dochkr1  34754  dochkr1OLDN  34755  lcfl6lem  34774  lcfl9a  34781  lclkrlem2l  34794  lclkrlem2o  34797  lclkrlem2q  34799  lcfrlem9  34826  lcfrlem16  34834  lcfrlem17  34835  lcfrlem27  34845  lcfrlem37  34855  lcfrlem38  34856  lcfrlem40  34858  lcdlkreqN  34898  mapdrvallem2  34921  mapdn0  34945  mapdpglem20  34967  mapdpglem30  34978  mapdindp0  34995  mapdhcl  35003  mapdh6aN  35011  mapdh6dN  35015  mapdh6eN  35016  mapdh6kN  35022  mapdh8  35065  hdmap1l6a  35086  hdmap1l6d  35090  hdmap1l6e  35091  hdmap1l6k  35097  hdmapval3N  35117  hdmap10  35119  hdmap11lem2  35121  hdmapnzcl  35124  hdmaprnlem3eN  35137  hdmaprnlem17N  35142  hdmap14lem4a  35150  hdmap14lem7  35153  hdmap14lem14  35160  hgmaprnlem5N  35179  hdmaplkr  35192  hdmapip0  35194  hgmapvvlem2  35203  hgmapvvlem3  35204  hgmapvv  35205  pellexlem5  35386  dfac11  35625  dfacbasgrp  35672  dgraalem  35709  dgraaub  35712  aaitgo  35726  sdrgacs  35765  cntzsdrg  35766  proot1ex  35776  isdomn3  35779  deg1mhm  35782  ofdivrec  36311  ofdivcan4  36312  ofdivdiv2  36313  expgrowth  36320  binomcxplemnotnn0  36341  dvrecg  37353  dvmptdiv  37360  dvdivbd  37366  dvdivcncf  37370  dirkeritg  37532  fourierdlem39  37576  fourierdlem57  37594  fourierdlem58  37595  fourierdlem59  37596  fourierdlem68  37605  fourierdlem76  37613  fourierdlem103  37640  fourierdlem104  37641  fourierdlem111  37648  oddprmALTV  38205  evenprm2  38231  elpwdifsn  38372  2zrngnmrid  38707  fdmdifeqresdif  38882  lincext1  39006  lindslinindsimp2lem5  39014  rege1logbrege0  39129  fllogbd  39131  relogbmulbexp  39132  relogbdivb  39133  nnpw2blen  39151  blennngt2o2  39163  blennn0e2  39165  dignn0ldlem  39173  aacllem  39300
  Copyright terms: Public domain W3C validator