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

Theorem eldifsn 3919
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 3322 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 3828 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2632 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C } 
<->  A  =/=  C ) )
43pm5.32i 619 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
51, 4bitri 241 1  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    /\ wa 359    e. wcel 1725    =/= wne 2598    \ cdif 3309   {csn 3806
This theorem is referenced by:  eldifsni  3920  rexdifsn  3923  difsn  3925  onmindif2  4784  sossfld  5309  fnniniseg2  5846  rexsupp  5847  suppss  5855  suppssr  5856  suppssfv  6293  suppssov1  6294  dif1o  6736  difsnen  7182  limenpsi  7274  frfi  7344  fofinf1o  7379  wemapso2  7513  dfac8clem  7905  acni2  7919  acndom  7924  acnnum  7925  dfac9  8008  dfacacn  8013  kmlem3  8024  kmlem4  8025  fin23lem21  8211  canthp1lem2  8520  elni  8745  mulnzcnopr  9660  divval  9672  elnnne0  10227  elq  10568  expcl2lem  11385  expclzlem  11397  reccn2  12382  rlimdiv  12431  eff2  12692  tanval  12721  rpnnen2lem9  12814  fzo0dvdseq  12894  4sqlem19  13323  prmlem0  13420  prmlem1a  13421  setsnid  13501  grpinvnzcl  14855  odcau  15230  efgsf  15353  efgsrel  15358  efgs1  15359  efgs1b  15360  efgsp1  15361  efgsres  15362  efgredlema  15364  efgredlemd  15368  efgrelexlemb  15374  gsumpt  15537  dmdprdd  15552  dprdcntz  15558  dprdfeq0  15572  dprd2da  15592  drngunit  15832  isdrng2  15837  drngid2  15843  isdrngd  15852  issubdrg  15885  abvtriv  15921  islss  16003  lssneln0  16020  lssssr  16021  lbsind  16144  lbspss  16146  lspabs3  16185  lspsneq  16186  lspfixed  16192  lspexch  16193  islbs2  16218  rrgsupp  16343  isdomn2  16351  domnrrg  16352  mvrcl  16504  coe1tmmul2  16660  cnflddiv  16723  cnfldinv  16724  xrs1mnd  16728  xrs10  16729  xrge0subm  16731  cnsubdrglem  16741  cnmsubglem  16753  gzrngunit  16756  zrngunit  16757  domnchr  16805  ist1-2  17403  cmpfi  17463  2ndcdisj  17511  2ndcsep  17514  alexsublem  18067  cldsubg  18132  imasdsf1olem  18395  prdsxmslem2  18551  reperflem  18841  xrge0gsumle  18856  xrge0tsms  18857  divcn  18890  evth  18976  cphreccllem  19133  bcthlem5  19273  itg11  19575  i1fmullem  19578  i1fadd  19579  itg1addlem2  19581  i1fmulc  19587  itg1mulc  19588  ellimc3  19758  limcmpt2  19763  dvlem  19775  dvidlem  19794  dvcnp  19797  dvcobr  19824  dvrec  19833  dvcnvlem  19852  dvexp3  19854  dveflem  19855  dvferm1lem  19860  dvferm2lem  19862  lhop1lem  19889  ftc1lem5  19916  mdegleb  19979  coe1mul3  20014  ply1nz  20036  fta1blem  20083  fta1b  20084  ig1peu  20086  ig1pdvds  20091  plyeq0lem  20121  dgrub  20145  quotval  20201  fta1lem  20216  fta1  20217  elqaalem3  20230  qaa  20232  iaa  20234  aareccl  20235  aannenlem2  20238  abelthlem8  20347  abelth  20349  reefgim  20358  eff1olem  20442  logrncl  20457  eflog  20466  logeftb  20470  logdmss  20525  dvlog  20534  angval  20635  dcubic  20678  rlimcnp  20796  efrlim  20800  logexprlim  21001  dchrghm  21032  dchrabs  21036  lgsfcl2  21078  lgsval2lem  21082  lgsval3  21090  lgsmod  21097  lgsdirprm  21105  lgsne0  21109  lgsquad2lem2  21135  2sqlem11  21151  2sqblem  21153  dchrvmaeq0  21190  rpvmasum2  21198  dchrisum0re  21199  qrngdiv  21310  umgra1  21353  uslgra1  21384  cusgrarn  21460  cusgrafilem2  21481  sizeusglecusglem1  21485  umgrabi  21697  ablomul  21935  mulid  21936  xdivval  24157  xrge0tsmsd  24215  logbcl  24389  logbid1  24390  rnlogbval  24392  relogbcl  24394  logb1  24395  nnlogbexp  24396  subfacp1lem5  24862  cvmsi  24944  cvmsval  24945  cvmsdisj  24949  cvmscld  24952  cvmsss2  24953  sinccvglem  25101  circum  25103  axlowdimlem9  25881  axlowdimlem12  25884  axlowdimlem13  25885  itg2addnclem2  26247  locfincmp  26365  sdclem1  26428  rrncmslem  26522  rrnequiv  26525  isdrngo2  26555  isdrngo3  26556  prtlem100  26685  prter2  26711  prter3  26712  raldifsni  26715  pellexlem5  26877  dfac11  27118  dfacbasgrp  27231  lindfind  27244  lindsind  27245  lindff1  27248  lindfrn  27249  dgraalem  27308  dgraaub  27311  aaitgo  27325  en2eleq  27339  en2other2  27340  f1omvdmvd  27344  pmtrprfv  27354  cnmsgngrp  27394  sdrgacs  27467  cntzsdrg  27468  proot1ex  27478  isdomn3  27481  deg1mhm  27484  ofdivrec  27501  ofdivcan4  27502  ofdivdiv2  27503  expgrowth  27510  2pthfrgra  28328  3cyclfrgrarn1  28329  n4cyclfrgra  28335  bnj158  29023  bnj168  29024  bnj529  29036  bnj906  29228  bnj970  29245  lsatlspsn2  29717  lsateln0  29720  lsatn0  29724  lsatspn0  29725  lsatcmp  29728  lsatelbN  29731  islshpat  29742  lsat0cv  29758  lkrlspeqN  29896  dvheveccl  31837  dihlatat  32062  dochnel  32118  dihjat1  32154  dvh4dimlem  32168  dochsnkr2cl  32199  dochkr1  32203  dochkr1OLDN  32204  lcfl6lem  32223  lcfl9a  32230  lclkrlem2l  32243  lclkrlem2o  32246  lclkrlem2q  32248  lcfrlem9  32275  lcfrlem16  32283  lcfrlem17  32284  lcfrlem27  32294  lcfrlem37  32304  lcfrlem38  32305  lcfrlem40  32307  lcdlkreqN  32347  mapdrvallem2  32370  mapdn0  32394  mapdpglem20  32416  mapdpglem30  32427  mapdindp0  32444  mapdhcl  32452  mapdh6aN  32460  mapdh6dN  32464  mapdh6eN  32465  mapdh6kN  32471  mapdh8  32514  hdmap1l6a  32535  hdmap1l6d  32539  hdmap1l6e  32540  hdmap1l6k  32546  hdmapval3N  32566  hdmap10  32568  hdmap11lem2  32570  hdmapnzcl  32573  hdmaprnlem3eN  32586  hdmaprnlem17N  32591  hdmap14lem4a  32599  hdmap14lem7  32602  hdmap14lem14  32609  hgmaprnlem5N  32628  hdmaplkr  32641  hdmapip0  32643  hgmapvvlem2  32652  hgmapvvlem3  32653  hgmapvv  32654
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-sn 3812
  Copyright terms: Public domain W3C validator