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

Theorem eleqtri 2355
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eleqtr.1  |-  A  e.  B
eleqtr.2  |-  B  =  C
Assertion
Ref Expression
eleqtri  |-  A  e.  C

Proof of Theorem eleqtri
StepHypRef Expression
1 eleqtr.1 . 2  |-  A  e.  B
2 eleqtr.2 . . 3  |-  B  =  C
32eleq2i 2347 . 2  |-  ( A  e.  B  <->  A  e.  C )
41, 3mpbi 199 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684
This theorem is referenced by:  eleqtrri  2356  3eltr3i  2361  prid2  3735  seqp1i  11062  faclbnd4lem1  11306  bcn1  11325  bcpasc  11333  cats1fv  11509  ef0lem  12360  phi1  12841  dfphi2  12842  gsumws1  14462  efgsp1  15046  efgsres  15047  efgredlemd  15053  efgredlem  15056  lt6abl  15181  indiscld  16828  cnrehmeo  18451  ovolicc1  18875  iblcnlem1  19142  dvcjbr  19298  c1lip2  19345  dvply1  19664  vieta1lem2  19691  dvtaylp  19749  taylthlem2  19753  dvloglem  19995  logdmopn  19996  efopnlem2  20004  logtayl  20007  cxpcn  20085  loglesqr  20098  leibpilem2  20237  log2ublem2  20243  efrlim  20264  basellem5  20322  ppiltx  20415  prmorcht  20416  chtlepsi  20445  chpub  20459  chebbnd1lem1  20618  chtppilimlem1  20622  nlelchi  22641  hmopidmchi  22731  ballotlemfrci  23086  ballotlemfrceq  23087  ballotlem1ri  23093  raddcn  23302  xrge0tmd  23328  indf  23599  konigsberg  23911  axlowdimlem16  24585  axlowdimlem17  24586  axlowdim  24589  bpoly2  24792  bpoly3  24793  bpoly4  24794  areacirclem4  24927  areacirclem5  24929  cncfres  26485  jm2.23  27089  uvcvvcl  27236  usgraexvlem  28127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator