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

Theorem eleq1a 2473
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 2464 . 2  |-  ( C  =  A  ->  ( C  e.  B  <->  A  e.  B ) )
21biimprcd 217 1  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721
This theorem is referenced by:  elex22  2927  elex2  2928  reu6  3083  disjne  3633  peano5  4827  ssimaex  5747  fnex  5920  f1ocnv2d  6254  tfrlem8  6604  tz7.48-2  6658  tz7.49  6661  eroprf  6961  onfin  7256  pssnn  7286  ac6sfi  7310  elfiun  7393  brwdom  7491  ficardom  7804  ficard  8396  tskxpss  8603  inar1  8606  rankcf  8608  tskuni  8614  gruun  8637  nsmallnq  8810  prnmadd  8830  genpss  8837  eqlei  9139  eqlei2  9140  renegcli  9318  supmul1  9929  supmullem2  9931  supmul  9932  nn0ind-raph  10326  uzwo  10495  uzwoOLD  10496  iccid  10917  hashvnfin  11597  brfi1indlem  11669  mertenslem2  12617  4sqlem1  13271  4sqlem4  13275  4sqlem11  13278  odlem1  15128  gexlem1  15168  lssneln0  15983  lss1d  15994  lspsn  16033  lsmelval2  16112  opnneiid  17145  cmpsublem  17416  metrest  18507  metustelOLD  18534  metustel  18535  dscopn  18574  ovolshftlem2  19359  subopnmbl  19449  deg1ldgn  19969  plyremlem  20174  coseq0negpitopi  20364  ppiublem1  20939  shsleji  22825  spansnss  23026  spansncvi  23107  f1o3d  23994  sigaclcu2  24456  measdivcstOLD  24531  dfon2lem6  25358  bdayfo  25543  altxpsspw  25726  mptelee  25738  hfun  26023  ontgval  26085  ordtoplem  26089  ordcmp  26101  findreccl  26107  supaddc  26137  supadd  26138  ovoliunnfl  26147  volsupnfl  26150  heibor1lem  26408  heibor1  26409  hbtlem2  27196  hbtlem5  27200  symggen  27279  psgnghm  27305  fveqvfvv  27855  afv0fv0  27880  frgrancvvdeqlem1  28133  frgrawopreglem4  28150  snssiALTVD  28648  snssiALT  28649  elex2VD  28659  elex22VD  28660  lshpkrlem1  29593  lfl1dim  29604  leat3  29778  meetat2  29780  glbconxN  29860  pointpsubN  30233  pmapglbx  30251  linepsubclN  30433  dia2dimlem7  31553  dib1dim2  31651  diclspsn  31677  dih1dimatlem  31812  dihatexv2  31822  djhlsmcl  31897
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-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator