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

Theorem eldifsn 4140
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 3471 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 4037 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2690 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C } 
<->  A  =/=  C ) )
43pm5.32i 637 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
51, 4bitri 249 1  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    /\ wa 369    e. wcel 1804    =/= wne 2638    \ cdif 3458   {csn 4014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-v 3097  df-dif 3464  df-sn 4015
This theorem is referenced by:  eldifsni  4141  rexdifsn  4144  raldifsni  4145  eldifvsn  4147  difsn  4149  sossfld  5444  fnniniseg2OLD  5996  rexsuppOLD  5997  suppssOLD  6005  suppssrOLD  6006  mpt2difsnif  6380  suppssfvOLD  6516  suppssov1OLD  6517  onmindif2  6632  mptsuppd  6925  suppssr  6933  suppssov1  6934  suppsssn  6937  suppssfv  6938  dif1o  7152  difsnen  7601  limenpsi  7694  frfi  7767  fofinf1o  7803  wemapso2OLD  7980  wemapso2lem  7981  en2eleq  8389  en2other2  8390  dfac8clem  8416  acni2  8430  acndom  8435  acnnum  8436  dfac9  8519  dfacacn  8524  kmlem3  8535  kmlem4  8536  fin23lem21  8722  canthp1lem2  9034  elni  9257  mulnzcnopr  10201  divval  10215  elnnne0  10815  elq  11193  expcl2lem  12157  expclzlem  12169  reccn2  13398  rlimdiv  13447  eff2  13711  tanval  13740  rpnnen2lem9  13833  fzo0dvdseq  13916  4sqlem19  14358  prmlem0  14468  prmlem1a  14469  setsnid  14551  grpinvnzcl  15984  symgextf  16316  symgextfv  16317  f1omvdmvd  16342  pmtrprfv  16352  odcau  16498  efgsf  16621  efgsrel  16626  efgs1  16627  efgs1b  16628  efgsp1  16629  efgsres  16630  efgredlema  16632  efgredlemd  16636  efgrelexlemb  16642  gsumpt  16862  gsumptOLD  16863  dmdprdd  16904  dprdcntz  16915  dprdfeq0  16936  dprdfeq0OLD  16943  dprd2da  16965  drngunit  17275  isdrng2  17280  drngid2  17286  isdrngd  17295  issubdrg  17328  abvtriv  17364  islss  17455  lssneln0  17472  lssssr  17473  lbsind  17600  lbspss  17602  lspabs3  17641  lspsneq  17642  lspfixed  17648  lspexch  17649  islbs2  17674  rrgsuppOLD  17814  isdomn2  17822  domnrrg  17823  mvrcl  17985  coe1tmmul2  18191  cnflddiv  18322  cnfldinv  18323  xrs1mnd  18330  xrs10  18331  xrge0subm  18333  cnsubdrglem  18343  cnmsubglem  18354  gzrngunit  18357  zringunit  18393  zrngunit  18394  domnchr  18442  cnmsgngrp  18488  psgninv  18491  psgndiflemB  18509  lindfind  18724  lindsind  18725  lindff1  18728  lindfrn  18729  mdetunilem9  18995  maducoeval2  19015  gsummatr01lem4  19033  ist1-2  19721  cmpfi  19781  2ndcdisj  19830  2ndcsep  19833  locfincmp  19900  alexsublem  20417  cldsubg  20482  imasdsf1olem  20749  prdsxmslem2  20905  reperflem  21196  xrge0gsumle  21211  xrge0tsms  21212  divcn  21245  evth  21332  cvsdiv  21482  cvsdivcl  21483  cphreccllem  21498  bcthlem5  21640  itg11  21971  i1fmullem  21974  i1fadd  21975  itg1addlem2  21977  i1fmulc  21983  itg1mulc  21984  ellimc3  22156  limcmpt2  22161  dvlem  22173  dvidlem  22192  dvcnp  22195  dvcobr  22222  dvrec  22231  dvcnvlem  22250  dvexp3  22252  dveflem  22253  dvferm1lem  22258  dvferm2lem  22260  lhop1lem  22287  ftc1lem5  22314  mdegleb  22337  coe1mul3  22373  ply1nz  22395  fta1blem  22442  fta1b  22443  ig1peu  22445  ig1pdvds  22450  plyeq0lem  22480  dgrub  22504  quotval  22560  fta1lem  22575  fta1  22576  elqaalem3  22589  qaa  22591  iaa  22593  aareccl  22594  aannenlem2  22597  abelthlem8  22706  abelth  22708  reefgim  22717  eff1olem  22807  logrncl  22827  eflog  22836  logeftb  22840  logdmss  22895  dvlog  22904  angval  23005  dcubic  23049  rlimcnp  23167  efrlim  23171  logexprlim  23372  dchrghm  23403  dchrabs  23407  lgsfcl2  23449  lgsval2lem  23453  lgsval3  23461  lgsmod  23468  lgsdirprm  23476  lgsne0  23480  lgsquad2lem2  23506  2sqlem11  23522  2sqblem  23524  dchrvmaeq0  23561  rpvmasum2  23569  dchrisum0re  23570  qrngdiv  23681  tglngval  23810  tgisline  23879  axlowdimlem9  24125  axlowdimlem12  24128  axlowdimlem13  24129  umgra1  24198  uslgra1  24244  cusgrarn  24331  cusgrafilem2  24352  sizeusglecusglem1  24356  nbhashuvtx  24788  umgrabi  24855  2pthfrgra  24883  3cyclfrgrarn1  24884  n4cyclfrgra  24890  ablomul  25229  mulid  25230  suppss3  27422  xdivval  27488  xrge0tsmsd  27648  ordtconlem1  27779  logbcl  27886  logbid1  27887  rnlogbval  27889  relogbcl  27891  logb1  27892  nnlogbexp  27893  sibfinima  28154  sseqf  28204  signswch  28391  signstfvn  28399  signsvtn0  28400  signstfvcl  28403  signstfveq0a  28406  signstfveq0  28407  signsvfn  28412  signsvtp  28413  signsvtn  28414  signsvfpn  28415  signsvfnn  28416  signlem0  28417  subfacp1lem5  28501  cvmsi  28583  cvmsval  28584  cvmsdisj  28588  cvmscld  28591  cvmsss2  28592  sinccvglem  28911  circum  28913  itg2addnclem2  30042  sdclem1  30211  rrncmslem  30303  rrnequiv  30306  isdrngo2  30336  isdrngo3  30337  prtlem100  30571  prter2  30597  prter3  30598  pellexlem5  30744  dfac11  30983  dfacbasgrp  31032  dgraalem  31070  dgraaub  31073  aaitgo  31087  sdrgacs  31126  cntzsdrg  31127  proot1ex  31137  isdomn3  31140  deg1mhm  31143  ofdivrec  31207  ofdivcan4  31208  ofdivdiv2  31209  expgrowth  31216  dvrecg  31611  dvmptdiv  31618  dvdivbd  31624  dvdivcncf  31628  dirkeritg  31773  fourierdlem39  31817  fourierdlem57  31835  fourierdlem58  31836  fourierdlem59  31837  fourierdlem68  31846  fourierdlem76  31854  fourierdlem103  31881  fourierdlem104  31882  fourierdlem111  31889  elpwdifsn  32134  tpres  32390  2zrngnmrid  32463  fdmdifeqresdif  32659  lincext1  32785  lindslinindsimp2lem5  32793  bnj158  33512  bnj168  33513  bnj529  33526  bnj906  33716  bnj970  33733  lsatlspsn2  34451  lsateln0  34454  lsatn0  34458  lsatspn0  34459  lsatcmp  34462  lsatelbN  34465  islshpat  34476  lsat0cv  34492  lkrlspeqN  34630  dvheveccl  36573  dihlatat  36798  dochnel  36854  dihjat1  36890  dvh4dimlem  36904  dochsnkr2cl  36935  dochkr1  36939  dochkr1OLDN  36940  lcfl6lem  36959  lcfl9a  36966  lclkrlem2l  36979  lclkrlem2o  36982  lclkrlem2q  36984  lcfrlem9  37011  lcfrlem16  37019  lcfrlem17  37020  lcfrlem27  37030  lcfrlem37  37040  lcfrlem38  37041  lcfrlem40  37043  lcdlkreqN  37083  mapdrvallem2  37106  mapdn0  37130  mapdpglem20  37152  mapdpglem30  37163  mapdindp0  37180  mapdhcl  37188  mapdh6aN  37196  mapdh6dN  37200  mapdh6eN  37201  mapdh6kN  37207  mapdh8  37250  hdmap1l6a  37271  hdmap1l6d  37275  hdmap1l6e  37276  hdmap1l6k  37282  hdmapval3N  37302  hdmap10  37304  hdmap11lem2  37306  hdmapnzcl  37309  hdmaprnlem3eN  37322  hdmaprnlem17N  37327  hdmap14lem4a  37335  hdmap14lem7  37338  hdmap14lem14  37345  hgmaprnlem5N  37364  hdmaplkr  37377  hdmapip0  37379  hgmapvvlem2  37388  hgmapvvlem3  37389  hgmapvv  37390
  Copyright terms: Public domain W3C validator