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

Theorem eleq1a 2507
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 2498 . 2  |-  ( C  =  A  ->  ( C  e.  B  <->  A  e.  B ) )
21biimprcd 218 1  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726
This theorem is referenced by:  elex22  2969  elex2  2970  reu6  3125  disjne  3675  peano5  4871  ssimaex  5791  fnex  5964  f1ocnv2d  6298  tfrlem8  6648  tz7.48-2  6702  tz7.49  6705  eroprf  7005  onfin  7300  pssnn  7330  ac6sfi  7354  elfiun  7438  brwdom  7538  ficardom  7853  ficard  8445  tskxpss  8652  inar1  8655  rankcf  8657  tskuni  8663  gruun  8686  nsmallnq  8859  prnmadd  8879  genpss  8886  eqlei  9188  eqlei2  9189  renegcli  9367  supmul1  9978  supmullem2  9980  supmul  9981  nn0ind-raph  10375  uzwo  10544  uzwoOLD  10545  iccid  10966  hashvnfin  11647  brfi1indlem  11719  mertenslem2  12667  4sqlem1  13321  4sqlem4  13325  4sqlem11  13328  odlem1  15178  gexlem1  15218  lssneln0  16033  lss1d  16044  lspsn  16083  lsmelval2  16162  opnneiid  17195  cmpsublem  17467  metrest  18559  metustelOLD  18586  metustel  18587  dscopn  18626  ovolshftlem2  19411  subopnmbl  19501  deg1ldgn  20021  plyremlem  20226  coseq0negpitopi  20416  ppiublem1  20991  shsleji  22877  spansnss  23078  spansncvi  23159  f1o3d  24046  sigaclcu2  24508  measdivcstOLD  24583  dfon2lem6  25420  bdayfo  25635  altxpsspw  25827  mptelee  25839  hfun  26124  ontgval  26186  ordtoplem  26190  ordcmp  26202  findreccl  26208  supaddc  26245  supadd  26246  ovoliunnfl  26260  volsupnfl  26263  heibor1lem  26532  heibor1  26533  hbtlem2  27319  hbtlem5  27323  symggen  27402  psgnghm  27428  fveqvfvv  27978  afv0fv0  28003  lswrdn0  28294  frgrancvvdeqlem1  28493  frgrawopreglem4  28510  snssiALTVD  29013  snssiALT  29014  elex2VD  29024  elex22VD  29025  lshpkrlem1  29982  lfl1dim  29993  leat3  30167  meetat2  30169  glbconxN  30249  pointpsubN  30622  pmapglbx  30640  linepsubclN  30822  dia2dimlem7  31942  dib1dim2  32040  diclspsn  32066  dih1dimatlem  32201  dihatexv2  32211  djhlsmcl  32286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-clel 2434
  Copyright terms: Public domain W3C validator