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

Theorem eleq1a 2550
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 2539 . 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 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462
This theorem is referenced by:  elex2  3125  elex22  3126  reu6  3292  disjne  3872  ssimaex  5930  fnex  6125  f1ocnv2d  6508  peano5  6701  tfrlem8  7050  tz7.48-2  7104  tz7.49  7107  eroprf  7406  onfin  7705  pssnn  7735  ac6sfi  7760  elfiun  7886  brwdom  7989  ficardom  8338  ficard  8936  tskxpss  9146  inar1  9149  rankcf  9151  tskuni  9157  gruun  9180  nsmallnq  9351  prnmadd  9371  genpss  9378  eqlei  9690  eqlei2  9691  renegcli  9876  supmul1  10504  supmullem2  10506  supmul  10507  nn0ind-raph  10957  uzwo  11140  uzwoOLD  11141  iccid  11570  hashvnfin  12393  brfi1indlem  12491  mertenslem2  13650  4sqlem1  14318  4sqlem4  14322  4sqlem11  14325  symggen  16288  psgnran  16333  odlem1  16352  gexlem1  16392  lssneln0  17378  lss1d  17389  lspsn  17428  lsmelval2  17511  psgnghm  18380  opnneiid  19390  cmpsublem  19662  metrest  20759  metustelOLD  20786  metustel  20787  dscopn  20826  ovolshftlem2  21653  subopnmbl  21745  deg1ldgn  22225  plyremlem  22431  coseq0negpitopi  22626  ppiublem1  23202  mptelee  23871  frgrancvvdeqlem1  24704  frgrawopreglem4  24721  shsleji  25961  spansnss  26162  spansncvi  26243  f1o3d  27141  sigaclcu2  27757  measdivcstOLD  27832  dfon2lem6  28794  bdayfo  29009  altxpsspw  29201  hfun  29409  ontgval  29470  ordtoplem  29474  ordcmp  29486  findreccl  29492  supaddc  29615  supadd  29616  ovoliunnfl  29631  volsupnfl  29634  heibor1lem  29906  heibor1  29907  hbtlem2  30677  hbtlem5  30681  fveqvfvv  31676  afv0fv0  31701  lswn0  31812  gsumpr  32014  snssiALTVD  32707  snssiALT  32708  elex2VD  32718  elex22VD  32719  bj-xpnzex  33597  bj-snsetex  33602  lshpkrlem1  33907  lfl1dim  33918  leat3  34092  meetat2  34094  glbconxN  34174  pointpsubN  34547  pmapglbx  34565  linepsubclN  34747  dia2dimlem7  35867  dib1dim2  35965  diclspsn  35991  dih1dimatlem  36126  dihatexv2  36136  djhlsmcl  36211
  Copyright terms: Public domain W3C validator