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

Theorem eqbrtrrd 4340
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
eqbrtrrd.1
eqbrtrrd.2
Assertion
Ref Expression
eqbrtrrd

Proof of Theorem eqbrtrrd
StepHypRef Expression
1 eqbrtrrd.1 . . 3
21eqcomd 2494 . 2
3 eqbrtrrd.2 . 2
42, 3eqbrtrd 4338 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  =wceq 1670   class class class wbr 4318
This theorem is referenced by:  dftpos4  6730  fodomfi  7551  cnfcom2lem  7825  infcda1  8244  enfin1ai  8435  fin56  8444  pwcfsdom  8629  fpwwe2lem7  8682  fpwwe2  8689  canthp1lem1  8698  1nqenq  9010  prlem936  9095  lemulge11  10060  supmul1  10161  xaddge0  11085  xadddi2  11124  ltexp2a  11764  leexp2a  11768  nnlesq  11818  digit1  11847  faclbnd4lem1  11918  faclbnd6  11924  facavg  11926  abs3dif  12666  abs2dif  12667  limsupgre  12806  rlimclim1  12870  rlimuni  12875  rlimres2  12886  rlimcn1  12913  rlimcn1b  12914  recn2  12925  imcn2  12926  rlimo1  12941  o1rlimmul  12943  iserex  12981  isercoll  12992  caucvgrlem2  12999  caucvgr  13000  iseraltlem3  13008  summolem2a  13040  fsumge1  13107  o1fsum  13123  isumrpcl  13153  climcnds  13161  harmonic  13168  mertenslem1  13191  ege2le3  13222  efgt1p2  13245  efgt1p  13246  eirrlem  13333  rpnnen2lem11  13354  fsumdvds  13423  bitsfzo  13478  bitsmod  13479  bitscmp  13481  mulgcd  13577  dvdssqlem  13590  nn0seqcvgd  13592  mulgcddvds  13637  rpdvds  13657  qden1elz  13682  phimullem  13701  pcdvdstr  13789  pockthg  13814  prmreclem1  13824  4sqlem11  13863  ramub1lem1  13934  ramub1lem2  13935  mreexexlem4d  14426  sscid  14578  latmlej21  15103  latmlej22  15104  lubel  15133  efginvrel1  15969  odadd2  16074  odadd  16075  gexexlem  16077  cyggex2  16116  ablfacrplem  16238  ablfac1c  16244  ablfac1eu  16246  pgpfac1lem3a  16249  isabvd  16524  znrrg  17471  lmcn2  18696  metrtri  19402  imasdsf1olem  19418  stdbdxmet  19560  nrmmetd  19637  nmmtri  19683  nlmvscnlem2  19736  blcvx  19844  recld2  19860  zdis  19862  opnreen  19877  cnheibor  19995  lebnumlem3  20003  nmoleub2lem3  20138  nmoleub2lem2  20139  nmoleub3  20142  ipcnlem2  20213  cmetcaulem  20256  cncmet  20290  minveclem4  20348  ovoliunlem1  20413  ovoliun2  20417  ovolscalem1  20424  ovolicopnf  20435  voliunlem2  20460  volsup  20465  ioorcl2  20479  uniiccvol  20487  uniioombllem4  20493  i1fd  20586  mbfi1fseqlem4  20623  itg2const2  20646  itg2eqa  20650  itg2split  20654  itg2i1fseqle  20659  itg2cnlem2  20667  dvcnv  20876  dveflem  20878  dvferm1lem  20883  dvlip2  20894  c1liplem1  20895  dvivthlem1  20907  lhop1lem  20912  dvcvx  20919  dvfsumle  20920  dvfsumabs  20922  dvfsumlem4  20928  dvfsumrlim2  20931  ftc1a  20936  deg1pwle  21057  fta1blem  21106  aalioulem3  21266  aaliou2b  21273  ulmbdd  21329  ulmdvlem1  21331  itgulm  21339  pserdvlem2  21359  abelthlem3  21364  abelthlem5  21366  abelthlem6  21367  abelthlem7  21369  tanregt0  21461  argimlt0  21528  logdivlti  21535  logcnlem3  21555  logcnlem4  21556  logtayl  21571  logtayl2  21573  cxple2  21608  cxpcn3lem  21651  cxpaddle  21656  isosctrlem1  21682  atantayl  21798  efrlim  21829  dfef2  21830  o1cxp  21834  cxp2lim  21836  divsqrsumo1  21843  amgmlem  21849  logdifbnd  21853  emcllem7  21861  harmonicbnd4  21870  fsumharmonic  21871  ftalem2  21877  basellem2  21885  basellem5  21888  basellem9  21892  vma1  21970  sqff1o  21986  fsumfldivdiaglem  21995  chtub  22017  fsumvma2  22019  chpchtsum  22024  chpub  22025  logfaclbnd  22027  logfacbnd3  22028  logfacrlim  22029  logexprlim  22030  bcmono  22082  bposlem2  22090  bposlem5  22093  bposlem6  22094  lgsne0  22138  lgsquadlem1  22159  lgsquadlem2  22160  2sqblem  22182  chebbnd1lem1  22184  chtppilimlem1  22188  chtppilimlem2  22189  chpchtlim  22194  rplogsumlem1  22199  dchrvmasumiflem1  22216  dchrisum0flblem2  22224  dchrisum0fno1  22226  dchrisum0re  22228  dchrisum0lem2a  22232  dchrisum0lem3  22234  dirith  22244  mulog2sumlem1  22249  mulog2sumlem2  22250  log2sumbnd  22259  selberglem2  22261  logdivbnd  22271  selberg3lem1  22272  selberg4lem1  22275  pntrsumbnd2  22282  pntrlog2bndlem1  22292  pntrlog2bndlem5  22296  pntrlog2bndlem6  22298  pntpbnd1a  22300  pntpbnd1  22301  pntpbnd2  22302  pntibndlem3  22307  pntlemb  22312  pntlemn  22315  pntlemr  22317  pntlemj  22318  pntlemf  22320  pntlemo  22322  ostth2lem3  22350  ostth3  22353  nvabs  23183  nvlmle  23209  smcnlem  23214  ubthlem2  23394  minvecolem4  23403  htthlem  23441  normpyc  23670  nmophmi  24557  hstle  24756  hstles  24757  stlei  24766  mul2lt0llt0  25170  mul2lt0lgt0  25171  xrge0npcan  25289  archirngz  25338  archiabllem1a  25340  archiabllem2a  25343  archiabllem2c  25344  ornglmulle  25434  orngrmulle  25435  esumpinfval  25702  esumpinfsum  25706  esumpcvgval  25707  dya2icoseg  25872  eulerpartlems  25917  sgnmulsgn  26082  signsply0  26103  lgamgulmlem2  26162  lgamgulmlem3  26163  lgamucov  26170  lgamcvg2  26187  gamcvg2  26192  rescon  26281  sinccvglem  26457  circum  26459  prodmolem2a  26599  btwnxfr  27329  supaddc  27598  mblfinlem3  27610  mblfinlem4  27611  dvtanlem  27621  itg2addnclem3  27625  ftc1anc  27655  nn0prpwlem  27697  csbren  27828  trirn  27829  isbnd3  27865  cntotbnd  27877  bfp  27905  rrndstprj2  27912  irrapxlem1  28311  irrapxlem4  28314  pell1qrgaplem  28362  pellfundglb  28374  rmspecfund  28398  monotoddzzfi  28431  rmynn  28447  jm2.24nn  28450  jm2.17c  28453  jm2.24  28454  acongeq  28474  jm2.20nn  28494  jm2.26lem3  28498  jm2.27a  28502  jm2.27c  28504  rmydioph  28511  jm3.1lem2  28515  frlmpwfi  28602  f1linds  28635  hashgcdlem  28747  hashgcdeq  28748  cncmpmax  28929  fmul01lt1lem2  28941  clim1fr1  28952  stoweidlem1  28975  stoweidlem11  28985  stoweidlem14  28988  stoweidlem24  28998  stoweidlem26  29000  wallispilem4  29042  wallispilem5  29043  stirlinglem1  29048  2leaddle2  29354  isosctrlem1ALT  30516  1cvrjat  31822  3atlem1  31830  3atlem6  31835  llnmlplnN  31886  2llnjaN  31913  2lplnja  31966  dalem57  32076  dalawlem11  32228  dalawlem12  32229  lhp2lt  32348  lhpj1  32369  lhpm0atN  32376  4atexlemex2  32418  lautm  32441  cdleme17b  32634  cdleme20j  32665  cdleme30a  32725  cdlemg4c  32959  cdlemg17a  33008  cdlemg31c  33046  trljco  33087  cdlemk46  33295  dia2dimlem2  33413  cdlemm10N  33466  cdlemn10  33554  dihmeetlem1N  33638  dihglblem5apreN  33639  dihmeetlem15N  33669  mapdat  34015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-rab 2768  df-v 3017  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-sn 3915  df-pr 3916  df-op 3918  df-br 4319
  Copyright terms: Public domain W3C validator