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

Theorem eleq1a 2427
Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
Assertion
Ref Expression
eleq1a  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )

Proof of Theorem eleq1a
StepHypRef Expression
1 eleq1 2418 . 2  |-  ( C  =  A  ->  ( C  e.  B  <->  A  e.  B ) )
21biimprcd 216 1  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    e. wcel 1710
This theorem is referenced by:  elex22  2875  elex2  2876  reu6  3030  disjne  3576  peano5  4761  ssimaex  5667  fnex  5827  f1ocnv2d  6155  tfrlem8  6487  tz7.48-2  6541  tz7.49  6544  eroprf  6844  onfin  7139  pssnn  7169  ac6sfi  7191  elfiun  7273  brwdom  7371  ficardom  7684  ficard  8277  tskxpss  8484  inar1  8487  rankcf  8489  tskuni  8495  gruun  8518  nsmallnq  8691  prnmadd  8711  genpss  8718  renegcli  9198  supmul1  9809  supmullem2  9811  supmul  9812  nn0ind-raph  10204  uzwo  10373  uzwoOLD  10374  iccid  10793  mertenslem2  12438  4sqlem1  13092  4sqlem4  13096  4sqlem11  13099  odlem1  14949  gexlem1  14989  lssneln0  15808  lss1d  15819  lspsn  15858  lsmelval2  15937  opnneiid  16969  cmpsublem  17232  metrest  18172  dscopn  18198  ovolshftlem2  18973  subopnmbl  19063  deg1ldgn  19583  plyremlem  19788  coseq0negpitopi  19978  ppiublem1  20553  shsleji  22063  spansnss  22264  spansncvi  22345  f1o3d  23245  sigaclcu2  23769  measdivcstOLD  23842  measdivcst  23843  gammadenomn0  24648  dfon2lem6  24702  bdayfo  24887  altxpsspw  25070  mptelee  25082  hfun  25367  ontgval  25429  ordtoplem  25433  ordcmp  25445  findreccl  25451  supaddc  25482  supadd  25483  ovoliunnfl  25488  volsupnfl  25491  heibor1lem  25856  heibor1  25857  hbtlem2  26651  hbtlem5  26655  symggen  26734  psgnghm  26760  fveqvfvv  27312  afv0fv0  27337  hashvnfin  27474  brfi1indlem  27496  frgrancvvdeqlem1  27863  frgrawopreglem4  27880  snssiALTVD  28364  snssiALT  28365  elex2VD  28376  elex22VD  28377  lshpkrlem1  29369  lfl1dim  29380  leat3  29554  meetat2  29556  glbconxN  29636  pointpsubN  30009  pmapglbx  30027  linepsubclN  30209  dia2dimlem7  31329  dib1dim2  31427  diclspsn  31453  dih1dimatlem  31588  dihatexv2  31598  djhlsmcl  31673
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2351  df-clel 2354
  Copyright terms: Public domain W3C validator