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

Theorem eleqtri 2543
Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)
Hypotheses
Ref Expression
eleqtr.1
eleqtr.2
Assertion
Ref Expression
eleqtri

Proof of Theorem eleqtri
StepHypRef Expression
1 eleqtr.1 . 2
2 eleqtr.2 . . 3
32eleq2i 2535 . 2
41, 3mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818
This theorem is referenced by:  eleqtrri  2544  3eltr3i  2557  prid2  4139  2eluzge0  11154  seqp1i  12123  faclbnd4lem1  12371  cats1fv  12824  ef0lem  13814  phi1  14303  gsumws1  16007  lt6abl  16897  uvcvvcl  18818  smadiadetlem4  19171  indiscld  19592  cnrehmeo  21453  ovolicc1  21927  dvcjbr  22352  vieta1lem2  22707  dvloglem  23029  logdmopn  23030  efopnlem2  23038  cxpcn  23119  loglesqrt  23132  log2ublem2  23278  efrlim  23299  axlowdimlem16  24260  axlowdimlem17  24261  usgraexvlem  24395  konigsberg  24987  nlelchi  26980  hmopidmchi  27070  raddcn  27911  xrge0tmd  27928  indf  28029  ballotlem1ri  28473  bpoly2  29819  bpoly3  29820  bpoly4  29821  dvtanlem  30064  ftc1cnnc  30089  dvasin  30103  dvacos  30104  dvreasin  30105  dvreacos  30106  areacirclem2  30108  areacirclem4  30110  cncfres  30261  jm2.23  30938  fourierdlem28  31917  fourierdlem57  31946  fourierdlem59  31948  fourierdlem62  31951  fourierdlem68  31957  fouriersw  32014  etransclem23  32040  etransclem35  32052  etransclem38  32055  etransclem39  32056  etransclem44  32061  etransclem45  32062  etransclem47  32064  frege54cor1c  37942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator