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 225 1  |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-clel 2434
This theorem is referenced by:  elex2  2979  elex22  2980  reu6  3143  disjne  3719  ssimaex  5751  fnex  5939  f1ocnv2d  6306  peano5  6494  tfrlem8  6835  tz7.48-2  6889  tz7.49  6892  eroprf  7190  onfin  7493  pssnn  7523  ac6sfi  7548  elfiun  7672  brwdom  7774  ficardom  8123  ficard  8721  tskxpss  8931  inar1  8934  rankcf  8936  tskuni  8942  gruun  8965  nsmallnq  9138  prnmadd  9158  genpss  9165  eqlei  9476  eqlei2  9477  renegcli  9662  supmul1  10287  supmullem2  10289  supmul  10290  nn0ind-raph  10734  uzwo  10909  uzwoOLD  10910  iccid  11337  hashvnfin  12121  brfi1indlem  12210  mertenslem2  13337  4sqlem1  14001  4sqlem4  14005  4sqlem11  14008  symggen  15967  psgnran  16012  odlem1  16029  gexlem1  16069  lssneln0  17013  lss1d  17024  lspsn  17063  lsmelval2  17146  psgnghm  17990  opnneiid  18710  cmpsublem  18982  metrest  20079  metustelOLD  20106  metustel  20107  dscopn  20146  ovolshftlem2  20973  subopnmbl  21064  deg1ldgn  21544  plyremlem  21750  coseq0negpitopi  21945  ppiublem1  22521  mptelee  23109  shsleji  24741  spansnss  24942  spansncvi  25023  f1o3d  25916  sigaclcu2  26532  measdivcstOLD  26607  dfon2lem6  27570  bdayfo  27785  altxpsspw  27977  hfun  28185  ontgval  28247  ordtoplem  28251  ordcmp  28263  findreccl  28269  supaddc  28388  supadd  28389  ovoliunnfl  28404  volsupnfl  28407  heibor1lem  28679  heibor1  28680  hbtlem2  29451  hbtlem5  29455  fveqvfvv  30001  afv0fv0  30026  lswn0  30229  frgrancvvdeqlem1  30594  frgrawopreglem4  30611  gsumpr  30727  snssiALTVD  31492  snssiALT  31493  elex2VD  31503  elex22VD  31504  bj-xpnzex  32351  bj-snsetex  32356  lshpkrlem1  32648  lfl1dim  32659  leat3  32833  meetat2  32835  glbconxN  32915  pointpsubN  33288  pmapglbx  33306  linepsubclN  33488  dia2dimlem7  34608  dib1dim2  34706  diclspsn  34732  dih1dimatlem  34867  dihatexv2  34877  djhlsmcl  34952
  Copyright terms: Public domain W3C validator