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

Theorem eleq1a 2502
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 2493 . 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 1362    e. wcel 1755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429
This theorem is referenced by:  elex2  2974  elex22  2975  reu6  3137  disjne  3712  ssimaex  5744  fnex  5931  f1ocnv2d  6300  peano5  6488  tfrlem8  6829  tz7.48-2  6883  tz7.49  6886  eroprf  7186  onfin  7489  pssnn  7519  ac6sfi  7544  elfiun  7668  brwdom  7770  ficardom  8119  ficard  8717  tskxpss  8927  inar1  8930  rankcf  8932  tskuni  8938  gruun  8961  nsmallnq  9134  prnmadd  9154  genpss  9161  eqlei  9472  eqlei2  9473  renegcli  9658  supmul1  10283  supmullem2  10285  supmul  10286  nn0ind-raph  10730  uzwo  10905  uzwoOLD  10906  iccid  11333  hashvnfin  12113  brfi1indlem  12202  mertenslem2  13328  4sqlem1  13992  4sqlem4  13996  4sqlem11  13999  symggen  15956  psgnran  16001  odlem1  16018  gexlem1  16058  lssneln0  16955  lss1d  16966  lspsn  17005  lsmelval2  17088  psgnghm  17852  opnneiid  18572  cmpsublem  18844  metrest  19941  metustelOLD  19968  metustel  19969  dscopn  20008  ovolshftlem2  20835  subopnmbl  20926  deg1ldgn  21449  plyremlem  21655  coseq0negpitopi  21850  ppiublem1  22426  mptelee  22964  shsleji  24596  spansnss  24797  spansncvi  24878  f1o3d  25772  sigaclcu2  26417  measdivcstOLD  26492  dfon2lem6  27448  bdayfo  27663  altxpsspw  27855  hfun  28063  ontgval  28125  ordtoplem  28129  ordcmp  28141  findreccl  28147  supaddc  28261  supadd  28262  ovoliunnfl  28277  volsupnfl  28280  heibor1lem  28552  heibor1  28553  hbtlem2  29325  hbtlem5  29329  fveqvfvv  29876  afv0fv0  29901  lswn0  30104  frgrancvvdeqlem1  30469  frgrawopreglem4  30486  gsumpr  30592  snssiALTVD  31265  snssiALT  31266  elex2VD  31276  elex22VD  31277  bj-xpnzex  32034  bj-snsetex  32039  lshpkrlem1  32328  lfl1dim  32339  leat3  32513  meetat2  32515  glbconxN  32595  pointpsubN  32968  pmapglbx  32986  linepsubclN  33168  dia2dimlem7  34288  dib1dim2  34386  diclspsn  34412  dih1dimatlem  34547  dihatexv2  34557  djhlsmcl  34632
  Copyright terms: Public domain W3C validator