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

Theorem eqbrtrrd 4474
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 2465 . 2
3 eqbrtrrd.2 . 2
42, 3eqbrtrd 4472 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  dftpos4  6993  fodomfi  7819  resfifsupp  7877  cnfcom2lem  8166  cnfcom2lemOLD  8174  infcda1  8594  enfin1ai  8785  fin56  8794  pwcfsdom  8979  fpwwe2lem7  9035  fpwwe2  9042  canthp1lem1  9051  1nqenq  9361  prlem936  9446  lemulge11  10429  supmul1  10533  xaddge0  11479  xadddi2  11518  ltexp2a  12217  leexp2a  12221  nnlesq  12271  digit1  12300  faclbnd4lem1  12371  faclbnd6  12377  facavg  12379  abs3dif  13164  abs2dif  13165  limsupgre  13304  rlimclim1  13368  rlimuni  13373  rlimres2  13384  rlimcn1  13411  rlimcn1b  13412  recn2  13423  imcn2  13424  rlimo1  13439  o1rlimmul  13441  iserex  13479  isercoll  13490  caucvgrlem2  13497  caucvgr  13498  iseraltlem3  13506  summolem2a  13537  fsumge1  13611  o1fsum  13627  isumrpcl  13655  climcnds  13663  harmonic  13670  mertenslem1  13693  prodmolem2a  13741  ege2le3  13825  efgt1p2  13849  efgt1p  13850  eirrlem  13937  rpnnen2lem11  13958  fsumdvds  14029  bitsfzo  14085  bitsmod  14086  bitscmp  14088  mulgcd  14184  dvdssqlem  14197  nn0seqcvgd  14199  mulgcddvds  14245  rpdvds  14265  qden1elz  14290  phimullem  14309  pcdvdstr  14399  pockthg  14424  prmreclem1  14434  4sqlem11  14473  ramub1lem1  14544  ramub1lem2  14545  mreexexlem4d  15044  sscid  15193  latmlej21  15722  latmlej22  15723  lubel  15752  efginvrel1  16746  odadd2  16855  odadd  16856  gexexlem  16858  cyggex2  16899  ablfacrplem  17116  ablfac1c  17122  ablfac1eu  17124  pgpfac1lem3a  17127  isabvd  17469  mptscmfsuppd  17577  znrrg  18604  frlmphl  18812  frlmup1  18832  f1linds  18860  chcoeffeqlem  19386  lmcn2  20150  metrtri  20860  imasdsf1olem  20876  stdbdxmet  21018  nrmmetd  21095  nmmtri  21141  nlmvscnlem2  21194  blcvx  21303  recld2  21319  zdis  21321  opnreen  21336  cnheibor  21455  lebnumlem3  21463  nmoleub2lem3  21598  nmoleub2lem2  21599  nmoleub3  21602  ipcnlem2  21684  cmetcaulem  21727  cncmet  21761  csbren  21826  trirn  21827  minveclem4  21847  ovoliunlem1  21913  ovoliun2  21917  ovolscalem1  21924  ovolicopnf  21935  voliunlem2  21961  volsup  21966  ioorcl2  21981  uniiccvol  21989  uniioombllem4  21995  i1fd  22088  mbfi1fseqlem4  22125  itg2const2  22148  itg2eqa  22152  itg2split  22156  itg2i1fseqle  22161  itg2cnlem2  22169  dvcnv  22378  dveflem  22380  dvferm1lem  22385  dvlip2  22396  c1liplem1  22397  dvivthlem1  22409  lhop1lem  22414  dvcvx  22421  dvfsumle  22422  dvfsumabs  22424  dvfsumlem4  22430  dvfsumrlim2  22433  ftc1a  22438  tdeglem4  22458  deg1pwle  22520  fta1blem  22569  aalioulem3  22730  aaliou2b  22737  ulmbdd  22793  ulmdvlem1  22795  itgulm  22803  pserdvlem2  22823  abelthlem3  22828  abelthlem5  22830  abelthlem6  22831  abelthlem7  22833  tanregt0  22926  argimlt0  22998  logdivlti  23005  logcnlem3  23025  logcnlem4  23026  logtayl  23041  logtayl2  23043  cxple2  23078  cxpcn3lem  23121  cxpaddle  23126  isosctrlem1  23152  atantayl  23268  efrlim  23299  dfef2  23300  o1cxp  23304  cxp2lim  23306  divsqrtsumo1  23313  amgmlem  23319  logdifbnd  23323  emcllem7  23331  harmonicbnd4  23340  fsumharmonic  23341  ftalem2  23347  basellem2  23355  basellem5  23358  basellem9  23362  vma1  23440  sqff1o  23456  fsumfldivdiaglem  23465  chtub  23487  fsumvma2  23489  chpchtsum  23494  chpub  23495  logfaclbnd  23497  logfacbnd3  23498  logfacrlim  23499  logexprlim  23500  bcmono  23552  bposlem2  23560  bposlem5  23563  bposlem6  23564  lgsne0  23608  lgsquadlem1  23629  lgsquadlem2  23630  2sqblem  23652  chebbnd1lem1  23654  chtppilimlem1  23658  chtppilimlem2  23659  chpchtlim  23664  rplogsumlem1  23669  dchrvmasumiflem1  23686  dchrisum0flblem2  23694  dchrisum0fno1  23696  dchrisum0re  23698  dchrisum0lem2a  23702  dchrisum0lem3  23704  dirith  23714  mulog2sumlem1  23719  mulog2sumlem2  23720  log2sumbnd  23729  selberglem2  23731  logdivbnd  23741  selberg3lem1  23742  selberg4lem1  23745  pntrsumbnd2  23752  pntrlog2bndlem1  23762  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntibndlem3  23777  pntlemb  23782  pntlemn  23785  pntlemr  23787  pntlemj  23788  pntlemf  23790  pntlemo  23792  ostth2lem3  23820  ostth3  23823  nehash2  23899  footeq  24098  hlperpnel  24099  perpdragALT  24101  perpdrag  24102  colperp  24103  mideulem2  24108  opphllem  24109  opphllem3  24121  lmieu  24150  nvabs  25576  nvlmle  25602  smcnlem  25607  ubthlem2  25787  minvecolem4  25796  htthlem  25834  normpyc  26063  nmophmi  26950  hstle  27149  hstles  27150  stlei  27159  mul2lt0llt0  27567  mul2lt0lgt0  27568  2sqmod  27636  xrge0npcan  27684  archirngz  27733  archiabllem1a  27735  archiabllem2a  27738  archiabllem2c  27739  ornglmulle  27795  orngrmulle  27796  esumpinfval  28079  esumpinfsum  28083  esumpcvgval  28084  dya2icoseg  28248  eulerpartlems  28299  sgnmulsgn  28488  signsplypnf  28507  signsply0  28508  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamucov  28580  lgamcvg2  28597  gamcvg2  28602  rescon  28691  sinccvglem  29038  circum  29040  btwnxfr  29706  supaddc  30041  mblfinlem3  30053  mblfinlem4  30054  dvtanlem  30064  itg2addnclem3  30068  ftc1anc  30098  nn0prpwlem  30140  isbnd3  30280  cntotbnd  30292  bfp  30320  rrndstprj2  30327  irrapxlem1  30758  irrapxlem4  30761  pell1qrgaplem  30809  pellfundglb  30821  rmspecfund  30845  monotoddzzfi  30878  rmynn  30894  jm2.24nn  30897  jm2.17c  30900  jm2.24  30901  acongeq  30921  jm2.20nn  30939  jm2.26lem3  30943  jm2.27a  30947  jm2.27c  30949  rmydioph  30956  jm3.1lem2  30960  frlmpwfi  31046  hashgcdlem  31157  hashgcdeq  31158  areaquad  31184  cvgdvgrat  31194  radcnvrat  31195  hashnzfzclim  31227  cncmpmax  31407  iooabslt  31532  fmul01lt1lem2  31579  clim1fr1  31607  limcrecl  31635  stoweidlem1  31783  stoweidlem11  31793  stoweidlem14  31796  stoweidlem24  31806  stoweidlem26  31808  wallispilem4  31850  wallispilem5  31851  stirlinglem1  31856  fourierdlem51  31940  fourierdlem65  31954  fouriersw  32014  2leaddle2  32320  isosctrlem1ALT  33734  1cvrjat  35199  3atlem1  35207  3atlem6  35212  llnmlplnN  35263  2llnjaN  35290  2lplnja  35343  dalem57  35453  dalawlem11  35605  dalawlem12  35606  lhp2lt  35725  lhpj1  35746  lhpm0atN  35753  4atexlemex2  35795  lautm  35818  cdleme17b  36012  cdleme20j  36044  cdleme30a  36104  cdlemg4c  36338  cdlemg17a  36387  cdlemg31c  36425  trljco  36466  cdlemk46  36674  dia2dimlem2  36792  cdlemm10N  36845  cdlemn10  36933  dihmeetlem1N  37017  dihglblem5apreN  37018  dihmeetlem15N  37048  mapdat  37394  rp-isfinite6  37744  imo72b2  37993
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-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator