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

Theorem eleq1a 2540
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 2529 . 2  |-  ( C  =  A  ->  ( C  e.  B  <->  A  e.  B ) )
21biimprcd 225 1  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1395    e. wcel 1819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-cleq 2449  df-clel 2452
This theorem is referenced by:  elex2  3121  elex22  3122  reu6  3288  disjne  3875  ssimaex  5938  fnex  6140  f1ocnv2d  6525  peano5  6722  tfrlem8  7071  tz7.48-2  7125  tz7.49  7128  eroprf  7427  onfin  7727  pssnn  7757  ac6sfi  7782  elfiun  7908  brwdom  8011  ficardom  8359  ficard  8957  tskxpss  9167  inar1  9170  rankcf  9172  tskuni  9178  gruun  9201  nsmallnq  9372  prnmadd  9392  genpss  9399  eqlei  9711  eqlei2  9712  renegcli  9899  supmul1  10528  supmullem2  10530  supmul  10531  nn0ind-raph  10985  uzwo  11169  uzwoOLD  11170  iccid  11599  hashvnfin  12434  brfi1indlem  12535  mertenslem2  13706  4sqlem1  14478  4sqlem4  14482  4sqlem11  14485  symggen  16622  psgnran  16667  odlem1  16686  gexlem1  16726  lssneln0  17725  lss1d  17736  lspsn  17775  lsmelval2  17858  psgnghm  18743  opnneiid  19754  cmpsublem  20026  metrest  21153  metustelOLD  21180  metustel  21181  dscopn  21220  ovolshftlem2  22047  subopnmbl  22139  deg1ldgn  22619  plyremlem  22826  coseq0negpitopi  23022  ppiublem1  23603  mptelee  24325  frgrancvvdeqlem1  25157  frgrawopreglem4  25174  shsleji  26415  spansnss  26616  spansncvi  26697  f1o3d  27618  sigaclcu2  28293  measdivcstOLD  28368  dfon2lem6  29437  bdayfo  29652  altxpsspw  29832  hfun  30040  ontgval  30101  ordtoplem  30105  ordcmp  30117  findreccl  30123  supaddc  30246  supadd  30247  ovoliunnfl  30261  volsupnfl  30264  heibor1lem  30510  heibor1  30511  hbtlem2  31277  hbtlem5  31281  fveqvfvv  32412  afv0fv0  32437  lswn0  32496  lidlmmgm  32875  1neven  32882  cznrng  32907  gsumpr  33094  snssiALTVD  33770  snssiALT  33771  elex2VD  33781  elex22VD  33782  bj-xpnzex  34659  bj-snsetex  34664  lshpkrlem1  34978  lfl1dim  34989  leat3  35163  meetat2  35165  glbconxN  35245  pointpsubN  35618  pmapglbx  35636  linepsubclN  35818  dia2dimlem7  36940  dib1dim2  37038  diclspsn  37064  dih1dimatlem  37199  dihatexv2  37209  djhlsmcl  37284  rp-isfinite6  37904
  Copyright terms: Public domain W3C validator