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

Theorem eldifsn 4107
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 3445 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 4007 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2698 . . 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 1758    =/= wne 2647    \ cdif 3432   {csn 3984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-v 3078  df-dif 3438  df-sn 3985
This theorem is referenced by:  eldifsni  4108  rexdifsn  4111  raldifsni  4112  eldifvsn  4113  difsn  4115  sossfld  5392  fnniniseg2OLD  5935  rexsuppOLD  5936  suppssOLD  5944  suppssrOLD  5945  mpt2difsnif  6292  suppssfvOLD  6425  suppssov1OLD  6426  onmindif2  6532  mptsuppd  6821  suppssr  6829  suppssov1  6830  suppsssn  6833  suppssfv  6834  dif1o  7049  difsnen  7502  limenpsi  7595  frfi  7667  fofinf1o  7702  wemapso2OLD  7876  wemapso2lem  7877  en2eleq  8285  en2other2  8286  dfac8clem  8312  acni2  8326  acndom  8331  acnnum  8332  dfac9  8415  dfacacn  8420  kmlem3  8431  kmlem4  8432  fin23lem21  8618  canthp1lem2  8930  elni  9155  mulnzcnopr  10092  divval  10106  elnnne0  10703  elq  11065  expcl2lem  11993  expclzlem  12005  reccn2  13191  rlimdiv  13240  eff2  13500  tanval  13529  rpnnen2lem9  13622  fzo0dvdseq  13703  4sqlem19  14141  prmlem0  14250  prmlem1a  14251  setsnid  14333  grpinvnzcl  15716  symgextf  16040  symgextfv  16041  f1omvdmvd  16067  pmtrprfv  16077  odcau  16223  efgsf  16346  efgsrel  16351  efgs1  16352  efgs1b  16353  efgsp1  16354  efgsres  16355  efgredlema  16357  efgredlemd  16361  efgrelexlemb  16367  gsumpt  16575  gsumptOLD  16576  dmdprdd  16602  dprdcntz  16613  dprdfeq0  16633  dprdfeq0OLD  16640  dprd2da  16662  drngunit  16959  isdrng2  16964  drngid2  16970  isdrngd  16979  issubdrg  17012  abvtriv  17048  islss  17138  lssneln0  17155  lssssr  17156  lbsind  17283  lbspss  17285  lspabs3  17324  lspsneq  17325  lspfixed  17331  lspexch  17332  islbs2  17357  rrgsuppOLD  17485  isdomn2  17493  domnrrg  17494  mvrcl  17651  coe1tmmul2  17852  cnflddiv  17970  cnfldinv  17971  xrs1mnd  17975  xrs10  17976  xrge0subm  17978  cnsubdrglem  17988  cnmsubglem  17999  gzrngunit  18002  zringunit  18038  zrngunit  18039  domnchr  18087  cnmsgngrp  18133  psgninv  18136  psgndiflemB  18154  lindfind  18369  lindsind  18370  lindff1  18373  lindfrn  18374  mdetunilem9  18557  maducoeval2  18577  gsummatr01lem4  18595  ist1-2  19082  cmpfi  19142  2ndcdisj  19191  2ndcsep  19194  alexsublem  19747  cldsubg  19812  imasdsf1olem  20079  prdsxmslem2  20235  reperflem  20526  xrge0gsumle  20541  xrge0tsms  20542  divcn  20575  evth  20662  cvsdiv  20812  cvsdivcl  20813  cphreccllem  20828  bcthlem5  20970  itg11  21301  i1fmullem  21304  i1fadd  21305  itg1addlem2  21307  i1fmulc  21313  itg1mulc  21314  ellimc3  21486  limcmpt2  21491  dvlem  21503  dvidlem  21522  dvcnp  21525  dvcobr  21552  dvrec  21561  dvcnvlem  21580  dvexp3  21582  dveflem  21583  dvferm1lem  21588  dvferm2lem  21590  lhop1lem  21617  ftc1lem5  21644  mdegleb  21667  coe1mul3  21703  ply1nz  21725  fta1blem  21772  fta1b  21773  ig1peu  21775  ig1pdvds  21780  plyeq0lem  21810  dgrub  21834  quotval  21890  fta1lem  21905  fta1  21906  elqaalem3  21919  qaa  21921  iaa  21923  aareccl  21924  aannenlem2  21927  abelthlem8  22036  abelth  22038  reefgim  22047  eff1olem  22136  logrncl  22151  eflog  22160  logeftb  22164  logdmss  22219  dvlog  22228  angval  22329  dcubic  22373  rlimcnp  22491  efrlim  22495  logexprlim  22696  dchrghm  22727  dchrabs  22731  lgsfcl2  22773  lgsval2lem  22777  lgsval3  22785  lgsmod  22792  lgsdirprm  22800  lgsne0  22804  lgsquad2lem2  22830  2sqlem11  22846  2sqblem  22848  dchrvmaeq0  22885  rpvmasum2  22893  dchrisum0re  22894  qrngdiv  23005  tglngval  23120  tgisline  23171  axlowdimlem9  23347  axlowdimlem12  23350  axlowdimlem13  23351  umgra1  23411  uslgra1  23442  cusgrarn  23518  cusgrafilem2  23539  sizeusglecusglem1  23543  umgrabi  23755  ablomul  23993  mulid  23994  suppss3  26177  xdivval  26238  xrge0tsmsd  26397  ordtconlem1  26498  logbcl  26600  logbid1  26601  rnlogbval  26603  relogbcl  26605  logb1  26606  nnlogbexp  26607  sibfinima  26868  sseqf  26918  signswch  27105  signstfvn  27113  signsvtn0  27114  signstfvneq0  27116  signstfvcl  27117  signstfveq0a  27120  signstfveq0  27121  signsvfn  27126  signsvtp  27127  signsvtn  27128  signsvfpn  27129  signsvfnn  27130  signlem0  27131  subfacp1lem5  27215  cvmsi  27297  cvmsval  27298  cvmsdisj  27302  cvmscld  27305  cvmsss2  27306  sinccvglem  27460  circum  27462  itg2addnclem2  28591  locfincmp  28723  sdclem1  28786  rrncmslem  28878  rrnequiv  28881  isdrngo2  28911  isdrngo3  28912  prtlem100  29147  prter2  29173  prter3  29174  pellexlem5  29321  dfac11  29562  dfacbasgrp  29611  dgraalem  29649  dgraaub  29652  aaitgo  29666  sdrgacs  29705  cntzsdrg  29706  proot1ex  29716  isdomn3  29719  deg1mhm  29722  ofdivrec  29747  ofdivcan4  29748  ofdivdiv2  29749  expgrowth  29756  nbhashuvtx  30681  2pthfrgra  30750  3cyclfrgrarn1  30751  n4cyclfrgra  30757  fdmdifeqresdif  30879  lincext1  31106  lindslinindsimp2lem5  31114  bnj158  32037  bnj168  32038  bnj529  32050  bnj906  32240  bnj970  32257  lsatlspsn2  32960  lsateln0  32963  lsatn0  32967  lsatspn0  32968  lsatcmp  32971  lsatelbN  32974  islshpat  32985  lsat0cv  33001  lkrlspeqN  33139  dvheveccl  35080  dihlatat  35305  dochnel  35361  dihjat1  35397  dvh4dimlem  35411  dochsnkr2cl  35442  dochkr1  35446  dochkr1OLDN  35447  lcfl6lem  35466  lcfl9a  35473  lclkrlem2l  35486  lclkrlem2o  35489  lclkrlem2q  35491  lcfrlem9  35518  lcfrlem16  35526  lcfrlem17  35527  lcfrlem27  35537  lcfrlem37  35547  lcfrlem38  35548  lcfrlem40  35550  lcdlkreqN  35590  mapdrvallem2  35613  mapdn0  35637  mapdpglem20  35659  mapdpglem30  35670  mapdindp0  35687  mapdhcl  35695  mapdh6aN  35703  mapdh6dN  35707  mapdh6eN  35708  mapdh6kN  35714  mapdh8  35757  hdmap1l6a  35778  hdmap1l6d  35782  hdmap1l6e  35783  hdmap1l6k  35789  hdmapval3N  35809  hdmap10  35811  hdmap11lem2  35813  hdmapnzcl  35816  hdmaprnlem3eN  35829  hdmaprnlem17N  35834  hdmap14lem4a  35842  hdmap14lem7  35845  hdmap14lem14  35852  hgmaprnlem5N  35871  hdmaplkr  35884  hdmapip0  35886  hgmapvvlem2  35895  hgmapvvlem3  35896  hgmapvv  35897
  Copyright terms: Public domain W3C validator