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

Theorem eldifsn 3870
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 3273 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 3779 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2584 . . 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 1717    =/= wne 2550    \ cdif 3260   {csn 3757
This theorem is referenced by:  eldifsni  3871  rexdifsn  3874  difsn  3876  onmindif2  4732  sossfld  5257  fnniniseg2  5793  rexsupp  5794  suppss  5802  suppssr  5803  suppssfv  6240  suppssov1  6241  dif1o  6680  difsnen  7126  limenpsi  7218  frfi  7288  fofinf1o  7323  wemapso2  7454  dfac8clem  7846  acni2  7860  acndom  7865  acnnum  7866  dfac9  7949  dfacacn  7954  kmlem3  7965  kmlem4  7966  fin23lem21  8152  canthp1lem2  8461  elni  8686  mulnzcnopr  9600  divval  9612  elnnne0  10167  elq  10508  expcl2lem  11320  expclzlem  11332  reccn2  12317  rlimdiv  12366  eff2  12627  tanval  12656  rpnnen2lem9  12749  fzo0dvdseq  12829  4sqlem19  13258  prmlem0  13355  prmlem1a  13356  setsnid  13436  grpinvnzcl  14790  odcau  15165  efgsf  15288  efgsrel  15293  efgs1  15294  efgs1b  15295  efgsp1  15296  efgsres  15297  efgredlema  15299  efgredlemd  15303  efgrelexlemb  15309  gsumpt  15472  dmdprdd  15487  dprdcntz  15493  dprdfeq0  15507  dprd2da  15527  drngunit  15767  isdrng2  15772  drngid2  15778  isdrngd  15787  issubdrg  15820  abvtriv  15856  islss  15938  lssneln0  15955  lssssr  15956  lbsind  16079  lbspss  16081  lspabs3  16120  lspsneq  16121  lspfixed  16127  lspexch  16128  islbs2  16153  rrgsupp  16278  isdomn2  16286  domnrrg  16287  mvrcl  16439  coe1tmmul2  16595  cnflddiv  16654  cnfldinv  16655  xrs1mnd  16659  xrs10  16660  xrge0subm  16662  cnsubdrglem  16672  cnmsubglem  16684  gzrngunit  16687  zrngunit  16688  domnchr  16736  ist1-2  17333  cmpfi  17393  2ndcdisj  17440  2ndcsep  17443  alexsublem  17996  cldsubg  18061  imasdsf1olem  18311  prdsxmslem2  18449  reperflem  18720  xrge0gsumle  18735  xrge0tsms  18736  divcn  18769  evth  18855  cphreccllem  19012  bcthlem5  19150  itg11  19450  i1fmullem  19453  i1fadd  19454  itg1addlem2  19456  i1fmulc  19462  itg1mulc  19463  ellimc3  19633  limcmpt2  19638  dvlem  19650  dvidlem  19669  dvcnp  19672  dvcobr  19699  dvrec  19708  dvcnvlem  19727  dvexp3  19729  dveflem  19730  dvferm1lem  19735  dvferm2lem  19737  lhop1lem  19764  ftc1lem5  19791  mdegleb  19854  coe1mul3  19889  ply1nz  19911  fta1blem  19958  fta1b  19959  ig1peu  19961  ig1pdvds  19966  plyeq0lem  19996  dgrub  20020  quotval  20076  fta1lem  20091  fta1  20092  elqaalem3  20105  qaa  20107  iaa  20109  aareccl  20110  aannenlem2  20113  abelthlem8  20222  abelth  20224  reefgim  20233  eff1olem  20317  logrncl  20332  eflog  20341  logeftb  20345  logdmss  20400  dvlog  20409  angval  20510  dcubic  20553  rlimcnp  20671  efrlim  20675  logexprlim  20876  dchrghm  20907  dchrabs  20911  lgsfcl2  20953  lgsval2lem  20957  lgsval3  20965  lgsmod  20972  lgsdirprm  20980  lgsne0  20984  lgsquad2lem2  21010  2sqlem11  21026  2sqblem  21028  dchrvmaeq0  21065  rpvmasum2  21073  dchrisum0re  21074  qrngdiv  21185  umgra1  21228  uslgra1  21259  cusgrarn  21334  cusgrafilem2  21355  sizeusglecusglem1  21359  umgrabi  21553  ablomul  21791  mulid  21792  xdivval  24003  xrge0tsmsd  24052  logbcl  24193  logbid1  24194  rnlogbval  24196  relogbcl  24198  logb1  24199  nnlogbexp  24200  subfacp1lem5  24649  cvmsi  24731  cvmsval  24732  cvmsdisj  24736  cvmscld  24739  cvmsss2  24740  sinccvglem  24888  circum  24890  axlowdimlem9  25603  axlowdimlem12  25606  axlowdimlem13  25607  itg2addnclem2  25958  locfincmp  26075  sdclem1  26138  rrncmslem  26232  rrnequiv  26235  isdrngo2  26265  isdrngo3  26266  prtlem100  26395  prter2  26421  prter3  26422  raldifsni  26425  pellexlem5  26587  dfac11  26829  dfacbasgrp  26942  lindfind  26955  lindsind  26956  lindff1  26959  lindfrn  26960  dgraalem  27019  dgraaub  27022  aaitgo  27036  en2eleq  27050  en2other2  27051  f1omvdmvd  27055  pmtrprfv  27065  cnmsgngrp  27105  sdrgacs  27178  cntzsdrg  27179  proot1ex  27189  isdomn3  27192  deg1mhm  27195  ofdivrec  27212  ofdivcan4  27213  ofdivdiv2  27214  expgrowth  27221  2pthfrgra  27764  3cyclfrgrarn1  27765  n4cyclfrgra  27771  bnj158  28434  bnj168  28435  bnj529  28447  bnj906  28639  bnj970  28656  lsatlspsn2  29107  lsateln0  29110  lsatn0  29114  lsatspn0  29115  lsatcmp  29118  lsatelbN  29121  islshpat  29132  lsat0cv  29148  lkrlspeqN  29286  dvheveccl  31227  dihlatat  31452  dochnel  31508  dihjat1  31544  dvh4dimlem  31558  dochsnkr2cl  31589  dochkr1  31593  dochkr1OLDN  31594  lcfl6lem  31613  lcfl9a  31620  lclkrlem2l  31633  lclkrlem2o  31636  lclkrlem2q  31638  lcfrlem9  31665  lcfrlem16  31673  lcfrlem17  31674  lcfrlem27  31684  lcfrlem37  31694  lcfrlem38  31695  lcfrlem40  31697  lcdlkreqN  31737  mapdrvallem2  31760  mapdn0  31784  mapdpglem20  31806  mapdpglem30  31817  mapdindp0  31834  mapdhcl  31842  mapdh6aN  31850  mapdh6dN  31854  mapdh6eN  31855  mapdh6kN  31861  mapdh8  31904  hdmap1l6a  31925  hdmap1l6d  31929  hdmap1l6e  31930  hdmap1l6k  31936  hdmapval3N  31956  hdmap10  31958  hdmap11lem2  31960  hdmapnzcl  31963  hdmaprnlem3eN  31976  hdmaprnlem17N  31981  hdmap14lem4a  31989  hdmap14lem7  31992  hdmap14lem14  31999  hgmaprnlem5N  32018  hdmaplkr  32031  hdmapip0  32033  hgmapvvlem2  32042  hgmapvvlem3  32043  hgmapvv  32044
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-v 2901  df-dif 3266  df-sn 3763
  Copyright terms: Public domain W3C validator