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

Theorem eleq1a 2544
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 2537 . 2  |-  ( C  =  A  ->  ( C  e.  B  <->  A  e.  B ) )
21biimprcd 233 1  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1452    e. wcel 1904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-cleq 2464  df-clel 2467
This theorem is referenced by:  elex2  3044  elex22  3045  reu6  3215  disjne  3814  ssimaex  5945  fnex  6148  f1ocnv2d  6539  peano5  6735  tfrlem8  7120  tz7.48-2  7177  tz7.49  7180  eroprf  7479  onfin  7781  pssnn  7808  ac6sfi  7833  elfiun  7962  brwdom  8100  ficardom  8413  ficard  9008  tskxpss  9215  inar1  9218  rankcf  9220  tskuni  9226  gruun  9249  nsmallnq  9420  prnmadd  9440  genpss  9447  eqlei  9762  eqlei2  9763  renegcli  9955  supaddc  10596  supadd  10597  supmul1  10598  supmullem2  10600  supmul  10601  nn0ind-raph  11058  uzwo  11245  iccid  11706  hashvnfin  12579  brfi1indlem  12690  mertenslem2  14018  4sqlem1  14971  4sqlem4  14975  4sqlem11  14978  symggen  17189  psgnran  17234  odlem1  17259  odlem1OLD  17262  gexlem1  17306  gexlem1OLD  17308  lssneln0  18253  lss1d  18264  lspsn  18303  lsmelval2  18386  psgnghm  19225  opnneiid  20219  cmpsublem  20491  metrest  21617  metustel  21643  dscopn  21666  ovolshftlem2  22541  subopnmbl  22641  deg1ldgn  23121  plyremlem  23336  coseq0negpitopi  23537  ppiublem1  24209  mptelee  25004  frgrancvvdeqlem1  25837  frgrawopreglem4  25854  shsleji  27104  spansnss  27305  spansncvi  27386  f1o3d  28305  sigaclcu2  29016  measdivcstOLD  29120  dfon2lem6  30505  bdayfo  30635  altxpsspw  30815  hfun  31016  ontgval  31162  ordtoplem  31166  ordcmp  31178  findreccl  31184  bj-xpnzex  31622  bj-snsetex  31627  topdifinfindis  31819  finxpreclem1  31851  ovoliunnfl  32046  volsupnfl  32049  heibor1lem  32205  heibor1  32206  lshpkrlem1  32747  lfl1dim  32758  leat3  32932  meetat2  32934  glbconxN  33014  pointpsubN  33387  pmapglbx  33405  linepsubclN  33587  dia2dimlem7  34709  dib1dim2  34807  diclspsn  34833  dih1dimatlem  34968  dihatexv2  34978  djhlsmcl  35053  hbtlem2  36054  hbtlem5  36058  rp-isfinite6  36234  snssiALTVD  37286  snssiALT  37287  elex2VD  37297  elex22VD  37298  fveqvfvv  38770  afv0fv0  38796  lswn0  39067  clel5  39128  nbuhgr2vtx1edgblem  39583  lidlmmgm  40433  1neven  40440  cznrng  40465  gsumpr  40650
  Copyright terms: Public domain W3C validator