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

Theorem eldifsn 4152
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 3486 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 4050 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2714 . . 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 1767    =/= wne 2662    \ cdif 3473   {csn 4027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-sn 4028
This theorem is referenced by:  eldifsni  4153  rexdifsn  4156  raldifsni  4157  eldifvsn  4159  difsn  4161  sossfld  5454  fnniniseg2OLD  6005  rexsuppOLD  6006  suppssOLD  6014  suppssrOLD  6015  mpt2difsnif  6379  suppssfvOLD  6515  suppssov1OLD  6516  onmindif2  6631  mptsuppd  6923  suppssr  6931  suppssov1  6932  suppsssn  6935  suppssfv  6936  dif1o  7150  difsnen  7599  limenpsi  7692  frfi  7765  fofinf1o  7801  wemapso2OLD  7977  wemapso2lem  7978  en2eleq  8386  en2other2  8387  dfac8clem  8413  acni2  8427  acndom  8432  acnnum  8433  dfac9  8516  dfacacn  8521  kmlem3  8532  kmlem4  8533  fin23lem21  8719  canthp1lem2  9031  elni  9254  mulnzcnopr  10195  divval  10209  elnnne0  10809  elq  11184  expcl2lem  12146  expclzlem  12158  reccn2  13382  rlimdiv  13431  eff2  13695  tanval  13724  rpnnen2lem9  13817  fzo0dvdseq  13898  4sqlem19  14340  prmlem0  14449  prmlem1a  14450  setsnid  14532  grpinvnzcl  15920  symgextf  16247  symgextfv  16248  f1omvdmvd  16274  pmtrprfv  16284  odcau  16430  efgsf  16553  efgsrel  16558  efgs1  16559  efgs1b  16560  efgsp1  16561  efgsres  16562  efgredlema  16564  efgredlemd  16568  efgrelexlemb  16574  gsumpt  16791  gsumptOLD  16792  dmdprdd  16833  dprdcntz  16844  dprdfeq0  16864  dprdfeq0OLD  16871  dprd2da  16893  drngunit  17201  isdrng2  17206  drngid2  17212  isdrngd  17221  issubdrg  17254  abvtriv  17290  islss  17381  lssneln0  17398  lssssr  17399  lbsind  17526  lbspss  17528  lspabs3  17567  lspsneq  17568  lspfixed  17574  lspexch  17575  islbs2  17600  rrgsuppOLD  17739  isdomn2  17747  domnrrg  17748  mvrcl  17910  coe1tmmul2  18116  cnflddiv  18247  cnfldinv  18248  xrs1mnd  18252  xrs10  18253  xrge0subm  18255  cnsubdrglem  18265  cnmsubglem  18276  gzrngunit  18279  zringunit  18315  zrngunit  18316  domnchr  18364  cnmsgngrp  18410  psgninv  18413  psgndiflemB  18431  lindfind  18646  lindsind  18647  lindff1  18650  lindfrn  18651  mdetunilem9  18917  maducoeval2  18937  gsummatr01lem4  18955  ist1-2  19642  cmpfi  19702  2ndcdisj  19751  2ndcsep  19754  alexsublem  20307  cldsubg  20372  imasdsf1olem  20639  prdsxmslem2  20795  reperflem  21086  xrge0gsumle  21101  xrge0tsms  21102  divcn  21135  evth  21222  cvsdiv  21372  cvsdivcl  21373  cphreccllem  21388  bcthlem5  21530  itg11  21861  i1fmullem  21864  i1fadd  21865  itg1addlem2  21867  i1fmulc  21873  itg1mulc  21874  ellimc3  22046  limcmpt2  22051  dvlem  22063  dvidlem  22082  dvcnp  22085  dvcobr  22112  dvrec  22121  dvcnvlem  22140  dvexp3  22142  dveflem  22143  dvferm1lem  22148  dvferm2lem  22150  lhop1lem  22177  ftc1lem5  22204  mdegleb  22227  coe1mul3  22263  ply1nz  22285  fta1blem  22332  fta1b  22333  ig1peu  22335  ig1pdvds  22340  plyeq0lem  22370  dgrub  22394  quotval  22450  fta1lem  22465  fta1  22466  elqaalem3  22479  qaa  22481  iaa  22483  aareccl  22484  aannenlem2  22487  abelthlem8  22596  abelth  22598  reefgim  22607  eff1olem  22696  logrncl  22711  eflog  22720  logeftb  22724  logdmss  22779  dvlog  22788  angval  22889  dcubic  22933  rlimcnp  23051  efrlim  23055  logexprlim  23256  dchrghm  23287  dchrabs  23291  lgsfcl2  23333  lgsval2lem  23337  lgsval3  23345  lgsmod  23352  lgsdirprm  23360  lgsne0  23364  lgsquad2lem2  23390  2sqlem11  23406  2sqblem  23408  dchrvmaeq0  23445  rpvmasum2  23453  dchrisum0re  23454  qrngdiv  23565  tglngval  23694  tgisline  23749  axlowdimlem9  23957  axlowdimlem12  23960  axlowdimlem13  23961  umgra1  24030  uslgra1  24076  cusgrarn  24163  cusgrafilem2  24184  sizeusglecusglem1  24188  nbhashuvtx  24620  umgrabi  24687  2pthfrgra  24715  3cyclfrgrarn1  24716  n4cyclfrgra  24722  ablomul  25061  mulid  25062  suppss3  27250  xdivval  27311  xrge0tsmsd  27466  ordtconlem1  27570  logbcl  27681  logbid1  27682  rnlogbval  27684  relogbcl  27686  logb1  27687  nnlogbexp  27688  sibfinima  27949  sseqf  27999  signswch  28186  signstfvn  28194  signsvtn0  28195  signstfvneq0  28197  signstfvcl  28198  signstfveq0a  28201  signstfveq0  28202  signsvfn  28207  signsvtp  28208  signsvtn  28209  signsvfpn  28210  signsvfnn  28211  signlem0  28212  subfacp1lem5  28296  cvmsi  28378  cvmsval  28379  cvmsdisj  28383  cvmscld  28386  cvmsss2  28387  sinccvglem  28541  circum  28543  itg2addnclem2  29672  locfincmp  29804  sdclem1  29867  rrncmslem  29959  rrnequiv  29962  isdrngo2  29992  isdrngo3  29993  prtlem100  30228  prter2  30254  prter3  30255  pellexlem5  30401  dfac11  30640  dfacbasgrp  30689  dgraalem  30727  dgraaub  30730  aaitgo  30744  sdrgacs  30783  cntzsdrg  30784  proot1ex  30794  isdomn3  30797  deg1mhm  30800  ofdivrec  30859  ofdivcan4  30860  ofdivdiv2  30861  expgrowth  30868  dvrecg  31268  dvmptdiv  31275  dvdivbd  31281  dvdivcncf  31285  dirkeritg  31430  fourierdlem39  31474  fourierdlem57  31492  fourierdlem58  31493  fourierdlem59  31494  fourierdlem68  31503  fourierdlem76  31511  fourierdlem103  31538  fourierdlem104  31539  fourierdlem111  31546  elpwdifsn  31791  fdmdifeqresdif  32027  lincext1  32154  lindslinindsimp2lem5  32162  bnj158  32882  bnj168  32883  bnj529  32895  bnj906  33085  bnj970  33102  lsatlspsn2  33807  lsateln0  33810  lsatn0  33814  lsatspn0  33815  lsatcmp  33818  lsatelbN  33821  islshpat  33832  lsat0cv  33848  lkrlspeqN  33986  dvheveccl  35927  dihlatat  36152  dochnel  36208  dihjat1  36244  dvh4dimlem  36258  dochsnkr2cl  36289  dochkr1  36293  dochkr1OLDN  36294  lcfl6lem  36313  lcfl9a  36320  lclkrlem2l  36333  lclkrlem2o  36336  lclkrlem2q  36338  lcfrlem9  36365  lcfrlem16  36373  lcfrlem17  36374  lcfrlem27  36384  lcfrlem37  36394  lcfrlem38  36395  lcfrlem40  36397  lcdlkreqN  36437  mapdrvallem2  36460  mapdn0  36484  mapdpglem20  36506  mapdpglem30  36517  mapdindp0  36534  mapdhcl  36542  mapdh6aN  36550  mapdh6dN  36554  mapdh6eN  36555  mapdh6kN  36561  mapdh8  36604  hdmap1l6a  36625  hdmap1l6d  36629  hdmap1l6e  36630  hdmap1l6k  36636  hdmapval3N  36656  hdmap10  36658  hdmap11lem2  36660  hdmapnzcl  36663  hdmaprnlem3eN  36676  hdmaprnlem17N  36681  hdmap14lem4a  36689  hdmap14lem7  36692  hdmap14lem14  36699  hgmaprnlem5N  36718  hdmaplkr  36731  hdmapip0  36733  hgmapvvlem2  36742  hgmapvvlem3  36743  hgmapvv  36744
  Copyright terms: Public domain W3C validator