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

Theorem eldifsn 3887
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 3290 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 3796 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2601 . . 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 1721    =/= wne 2567    \ cdif 3277   {csn 3774
This theorem is referenced by:  eldifsni  3888  rexdifsn  3891  difsn  3893  onmindif2  4751  sossfld  5276  fnniniseg2  5813  rexsupp  5814  suppss  5822  suppssr  5823  suppssfv  6260  suppssov1  6261  dif1o  6703  difsnen  7149  limenpsi  7241  frfi  7311  fofinf1o  7346  wemapso2  7477  dfac8clem  7869  acni2  7883  acndom  7888  acnnum  7889  dfac9  7972  dfacacn  7977  kmlem3  7988  kmlem4  7989  fin23lem21  8175  canthp1lem2  8484  elni  8709  mulnzcnopr  9624  divval  9636  elnnne0  10191  elq  10532  expcl2lem  11348  expclzlem  11360  reccn2  12345  rlimdiv  12394  eff2  12655  tanval  12684  rpnnen2lem9  12777  fzo0dvdseq  12857  4sqlem19  13286  prmlem0  13383  prmlem1a  13384  setsnid  13464  grpinvnzcl  14818  odcau  15193  efgsf  15316  efgsrel  15321  efgs1  15322  efgs1b  15323  efgsp1  15324  efgsres  15325  efgredlema  15327  efgredlemd  15331  efgrelexlemb  15337  gsumpt  15500  dmdprdd  15515  dprdcntz  15521  dprdfeq0  15535  dprd2da  15555  drngunit  15795  isdrng2  15800  drngid2  15806  isdrngd  15815  issubdrg  15848  abvtriv  15884  islss  15966  lssneln0  15983  lssssr  15984  lbsind  16107  lbspss  16109  lspabs3  16148  lspsneq  16149  lspfixed  16155  lspexch  16156  islbs2  16181  rrgsupp  16306  isdomn2  16314  domnrrg  16315  mvrcl  16467  coe1tmmul2  16623  cnflddiv  16686  cnfldinv  16687  xrs1mnd  16691  xrs10  16692  xrge0subm  16694  cnsubdrglem  16704  cnmsubglem  16716  gzrngunit  16719  zrngunit  16720  domnchr  16768  ist1-2  17365  cmpfi  17425  2ndcdisj  17472  2ndcsep  17475  alexsublem  18028  cldsubg  18093  imasdsf1olem  18356  prdsxmslem2  18512  reperflem  18802  xrge0gsumle  18817  xrge0tsms  18818  divcn  18851  evth  18937  cphreccllem  19094  bcthlem5  19234  itg11  19536  i1fmullem  19539  i1fadd  19540  itg1addlem2  19542  i1fmulc  19548  itg1mulc  19549  ellimc3  19719  limcmpt2  19724  dvlem  19736  dvidlem  19755  dvcnp  19758  dvcobr  19785  dvrec  19794  dvcnvlem  19813  dvexp3  19815  dveflem  19816  dvferm1lem  19821  dvferm2lem  19823  lhop1lem  19850  ftc1lem5  19877  mdegleb  19940  coe1mul3  19975  ply1nz  19997  fta1blem  20044  fta1b  20045  ig1peu  20047  ig1pdvds  20052  plyeq0lem  20082  dgrub  20106  quotval  20162  fta1lem  20177  fta1  20178  elqaalem3  20191  qaa  20193  iaa  20195  aareccl  20196  aannenlem2  20199  abelthlem8  20308  abelth  20310  reefgim  20319  eff1olem  20403  logrncl  20418  eflog  20427  logeftb  20431  logdmss  20486  dvlog  20495  angval  20596  dcubic  20639  rlimcnp  20757  efrlim  20761  logexprlim  20962  dchrghm  20993  dchrabs  20997  lgsfcl2  21039  lgsval2lem  21043  lgsval3  21051  lgsmod  21058  lgsdirprm  21066  lgsne0  21070  lgsquad2lem2  21096  2sqlem11  21112  2sqblem  21114  dchrvmaeq0  21151  rpvmasum2  21159  dchrisum0re  21160  qrngdiv  21271  umgra1  21314  uslgra1  21345  cusgrarn  21421  cusgrafilem2  21442  sizeusglecusglem1  21446  umgrabi  21658  ablomul  21896  mulid  21897  xdivval  24118  xrge0tsmsd  24176  logbcl  24350  logbid1  24351  rnlogbval  24353  relogbcl  24355  logb1  24356  nnlogbexp  24357  subfacp1lem5  24823  cvmsi  24905  cvmsval  24906  cvmsdisj  24910  cvmscld  24913  cvmsss2  24914  sinccvglem  25062  circum  25064  axlowdimlem9  25793  axlowdimlem12  25796  axlowdimlem13  25797  itg2addnclem2  26156  locfincmp  26274  sdclem1  26337  rrncmslem  26431  rrnequiv  26434  isdrngo2  26464  isdrngo3  26465  prtlem100  26594  prter2  26620  prter3  26621  raldifsni  26624  pellexlem5  26786  dfac11  27028  dfacbasgrp  27141  lindfind  27154  lindsind  27155  lindff1  27158  lindfrn  27159  dgraalem  27218  dgraaub  27221  aaitgo  27235  en2eleq  27249  en2other2  27250  f1omvdmvd  27254  pmtrprfv  27264  cnmsgngrp  27304  sdrgacs  27377  cntzsdrg  27378  proot1ex  27388  isdomn3  27391  deg1mhm  27394  ofdivrec  27411  ofdivcan4  27412  ofdivdiv2  27413  expgrowth  27420  2pthfrgra  28115  3cyclfrgrarn1  28116  n4cyclfrgra  28122  bnj158  28802  bnj168  28803  bnj529  28815  bnj906  29007  bnj970  29024  lsatlspsn2  29475  lsateln0  29478  lsatn0  29482  lsatspn0  29483  lsatcmp  29486  lsatelbN  29489  islshpat  29500  lsat0cv  29516  lkrlspeqN  29654  dvheveccl  31595  dihlatat  31820  dochnel  31876  dihjat1  31912  dvh4dimlem  31926  dochsnkr2cl  31957  dochkr1  31961  dochkr1OLDN  31962  lcfl6lem  31981  lcfl9a  31988  lclkrlem2l  32001  lclkrlem2o  32004  lclkrlem2q  32006  lcfrlem9  32033  lcfrlem16  32041  lcfrlem17  32042  lcfrlem27  32052  lcfrlem37  32062  lcfrlem38  32063  lcfrlem40  32065  lcdlkreqN  32105  mapdrvallem2  32128  mapdn0  32152  mapdpglem20  32174  mapdpglem30  32185  mapdindp0  32202  mapdhcl  32210  mapdh6aN  32218  mapdh6dN  32222  mapdh6eN  32223  mapdh6kN  32229  mapdh8  32272  hdmap1l6a  32293  hdmap1l6d  32297  hdmap1l6e  32298  hdmap1l6k  32304  hdmapval3N  32324  hdmap10  32326  hdmap11lem2  32328  hdmapnzcl  32331  hdmaprnlem3eN  32344  hdmaprnlem17N  32349  hdmap14lem4a  32357  hdmap14lem7  32360  hdmap14lem14  32367  hgmaprnlem5N  32386  hdmaplkr  32399  hdmapip0  32401  hgmapvvlem2  32410  hgmapvvlem3  32411  hgmapvv  32412
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-sn 3780
  Copyright terms: Public domain W3C validator