Theorem eqbrtrrd 5129

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

Step	Hyp	Ref	Expression
1		eqbrtrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2766	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 5127	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  dftpos4  8244  dif1en  9157  fodomfi  9283  fmptssfisupp  9365  cnfcom2lem  9681  dmttrcl  9701  ttrclselem2  9706  ficardadju  10203  enfin1ai  10387  pwcfsdom  10593  fpwwe2lem6  10646  fpwwe2  10653  canthp1lem1  10662  1nqenq  10972  prlem936  11057  lemulge11  12102  supaddc  12207  supmul1  12209  mul2lt0llt0  13149  mul2lt0lgt0  13150  xaddge0  13311  xadddi2  13350  ltexp2a  14231  leexp2a  14237  nnlesq  14270  digit1  14302  faclbnd4lem1  14358  faclbnd6  14364  facavg  14366  prsshashgt1  14476  nehash2  14540  sgnmulsgn  15183  abs3dif  15420  abs2dif  15421  limsupgre  15569  rlimclim1  15633  rlimuni  15638  rlimres2  15649  rlimcn1  15676  rlimcn1b  15677  recn2  15689  imcn2  15690  rlimo1  15705  o1rlimmul  15707  iserex  15745  isercoll  15756  caucvgrlem2  15763  caucvgr  15764  iseraltlem3  15772  summolem2a  15802  fsumge1  15885  o1fsum  15901  isumrpcl  15933  climcnds  15941  harmonic  15949  mertenslem1  15974  prodmolem2a  16022  ege2le3  16177  efgt1p2  16203  efgt1p  16204  eirrlem  16293  rpnnen2lem11  16313  fsumdvds  16399  bitsfzo  16526  bitsmod  16527  bitscmp  16529  mulgcd  16639  dvdssqlem  16657  nn0seqcvgd  16661  mulgcddvds  16746  rpdvds  16751  qden1elz  16849  phimullem  16871  hashgcdlem  16880  hashgcdeq  16882  pcdvdstr  16969  pockthg  16999  prmreclem1  17009  4sqlem11  17048  ramub1lem1  17119  ramub1lem2  17120  mreexexlem4d  17736  sscid  17914  latmlej21  18569  latmlej22  18570  lubel  18603  efginvrel1  19856  odadd2  19977  odadd  19978  gexexlem  19980  cyggex2  20025  ablfacrplem  20195  ablfac1c  20201  ablfac1eu  20203  pgpfac1lem3a  20206  isabvd  20979  ornglmulle  21034  orngrmulle  21035  mptscmfsuppd  21113  znrrg  21779  frlmphl  21995  frlmup1  22012  f1linds  22039  selvvvval  22359  psdmplcl  22391  chcoeffeqlem  23111  lmcn2  23876  metrtri  24584  imasdsf1olem  24600  stdbdxmet  24742  nrmmetd  24801  nmmtri  24849  nlmvscnlem2  24912  blcvx  25025  recld2  25042  zdis  25044  opnreen  25059  cnheibor  25184  lebnumlem3  25192  nmoleub2lem3  25344  nmoleub2lem2  25345  nmoleub3  25348  ipcnlem2  25473  cmetcaulem  25517  nglmle  25531  cncmet  25551  csbren  25628  trirn  25629  minveclem4  25661  ovoliunlem1  25731  ovoliun2  25735  ovolscalem1  25742  ovolicopnf  25753  voliunlem2  25780  volsup  25785  ioorcl2  25801  uniiccvol  25809  uniioombllem4  25815  i1fd  25910  mbfi1fseqlem4  25947  itg2const2  25970  itg2eqa  25974  itg2split  25978  itg2i1fseqle  25983  itg2cnlem2  25991  dvcnv  26205  dveflem  26207  dvferm1lem  26212  dvlip2  26223  c1liplem1  26224  dvivthlem1  26236  lhop1lem  26241  dvcvx  26248  dvfsumle  26249  dvfsumabs  26251  dvfsumlem4  26257  dvfsumrlim2  26260  ftc1a  26265  tdeglem4  26286  deg1pwle  26346  fta1blem  26397  aalioulem3  26571  aaliou2b  26578  ulmbdd  26635  ulmdvlem1  26637  itgulm  26645  pserdvlem2  26665  abelthlem3  26670  abelthlem5  26672  abelthlem6  26673  abelthlem7  26675  tanregt0  26777  argimlt0  26851  logdivlti  26858  logcnlem3  26882  logcnlem4  26883  logtayl  26898  logtayl2  26900  cxple2  26935  cxpcn3lem  26985  cxpaddle  26990  rtprmirr  26998  isosctrlem1  27056  atantayl  27175  efrlim  27207  dfef2  27208  o1cxp  27212  cxp2lim  27214  divsqrtsumo1  27221  amgmlem  27227  logdifbnd  27231  emcllem7  27239  harmonicbnd4  27248  fsumharmonic  27249  lgamgulmlem2  27267  lgamgulmlem3  27268  lgamucov  27275  lgamcvg2  27292  gamcvg2  27297  ftalem2  27311  basellem2  27319  basellem5  27322  basellem9  27326  vma1  27403  sqff1o  27419  fsumfldivdiaglem  27426  chtub  27449  fsumvma2  27451  chpchtsum  27456  chpub  27457  logfaclbnd  27459  logfacbnd3  27460  logfacrlim  27461  logexprlim  27462  bcmono  27514  bposlem2  27522  bposlem5  27525  bposlem6  27526  lgsne0  27572  lgsquadlem1  27617  lgsquadlem2  27618  2sqblem  27668  2sqmod  27673  chebbnd1lem1  27706  chtppilimlem1  27710  chtppilimlem2  27711  chpchtlim  27716  rplogsumlem1  27721  dchrvmasumiflem1  27738  dchrisum0flblem2  27746  dchrisum0fno1  27748  dchrisum0lem2a  27754  dchrisum0lem3  27756  dirith  27766  mulog2sumlem1  27771  mulog2sumlem2  27772  log2sumbnd  27781  selberglem2  27783  logdivbnd  27793  selberg3lem1  27794  selberg4lem1  27797  pntrsumbnd2  27804  pntrlog2bndlem1  27814  pntrlog2bndlem5  27818  pntrlog2bndlem6  27820  pntpbnd1a  27822  pntpbnd1  27823  pntpbnd2  27824  pntibndlem3  27829  pntlemb  27834  pntlemn  27837  pntlemr  27839  pntlemj  27840  pntlemf  27842  pntlemo  27844  ostth2lem3  27872  ostth3  27875  addsuniflem  28267  ltsp1d  28281  negsid  28307  negsunif  28321  negleft  28324  mulsuniflem  28415  precsexlem9  28481  n0sge0  28604  zcuts  28673  halfcut  28724  addhalfcut  28725  pw2cut2  28728  bdayfinbndlem1  28733  footeq  29079  hlperpnel  29081  perpdragALT  29083  perpdrag  29084  colperp  29085  mideulem2  29090  opphllem  29091  opphllem3  29105  lmieu  29169  trgcopy  29191  sacgr  29219  acopyeu  29222  perpeqlem  29227  angmgmaddcpbl  29270  perpprlng  29308  prlngmid2  29319  usgredgleordALT  29695  pthhashvtx  30195  eucrctshift  30724  nvabs  31154  smcnlem  31179  ubthlem2  31353  minvecolem4  31362  htthlem  31399  normpyc  31628  nmophmi  32513  hstle  32712  hstles  32713  stlei  32722  f1rnen  33102  nnmulge  33211  fsumiunle  33300  wrdt2ind  33396  xrge0npcan  33461  gsumwrd2dccat  33519  trsp2cyc  33564  archirngz  33630  archiabllem1a  33632  archiabllem2a  33635  archiabllem2c  33636  elrgspnlem1  33683  elrgspn  33687  elrgspnsubrunlem2  33689  rprmasso  33936  q1pdir  34014  r1pquslmic  34021  selvply1rhmlema  34029  selvply1rhmlem1  34031  evlextv  34053  mplvrpmga  34056  mplvrpmrhm  34058  drngdimgt0  34129  lbsdiflsp0  34137  fldextrspundgle  34189  fldext2rspun  34193  minplyirredlem  34221  madjusmdetlem2  34339  esumpinfval  34584  esumpinfsum  34588  esumpcvgval  34589  esum2d  34604  esumiun  34605  dya2icoseg  34789  omssubadd  34812  carsgsigalem  34827  carsggect  34830  carsgclctunlem3  34832  omsmeas  34835  eulerpartlems  34872  signsplypnf  35059  signsply0  35060  reprlt  35128  reprinfz1  35131  hgt750lemc  35156  hgt750lemf  35162  resconn  35826  sinccvglem  36252  circum  36254  btwnxfr  36637  nn0prpwlem  36942  dnibndlem2  37177  unblimceq0  37205  irrdiff  38079  poimirlem7  38377  mblfinlem3  38409  mblfinlem4  38410  itg2addnclem3  38423  ftc1anc  38451  isbnd3  38535  cntotbnd  38547  bfp  38575  rrndstprj2  38582  1cvrjat  40349  3atlem1  40357  3atlem6  40362  llnmlplnN  40413  2llnjaN  40440  2lplnja  40493  dalem57  40603  dalawlem11  40755  dalawlem12  40756  lhp2lt  40875  lhpj1  40896  lhpm0atN  40903  4atexlemex2  40945  lautm  40968  cdleme17b  41161  cdleme20j  41192  cdleme30a  41252  cdlemg4c  41486  cdlemg17a  41535  cdlemg31c  41573  trljco  41614  cdlemk46  41822  dia2dimlem2  41939  cdlemm10N  41992  cdlemn10  42080  dihmeetlem1N  42164  dihglblem5apreN  42165  dihmeetlem15N  42195  mapdat  42541  lcmineqlem19  42914  lcmineqlem20  42915  aks4d1p1p5  42942  aks4d1p8d2  42952  aks4d1p8  42954  aks4d1p9  42955  hashscontpow  42989  dvdsexpnn  43209  mullt0b1d  43372  evlselv  43436  mhphflem  43443  fltnlta  43510  3cubeslem1  43530  irrapxlem1  43664  irrapxlem4  43667  pell1qrgaplem  43715  pellfundglb  43727  rmspecfund  43751  monotoddzzfi  43784  rmynn  43798  jm2.24nn  43801  jm2.17c  43804  jm2.24  43805  acongeq  43825  jm2.20nn  43839  jm2.26lem3  43843  jm2.27a  43847  jm2.27c  43849  rmydioph  43856  jm3.1lem2  43860  frlmpwfi  43940  areaquad  44058  cantnf2  44167  rp-isfinite6  44359  frege129d  44604  leeq1d  44998  imo72b2lem0  45006  imo72b2  45013  cvgdvgrat  45138  radcnvrat  45139  hashnzfzclim  45147  isosctrlem1ALT  45757  cncmpmax  45867  iooabslt  46330  fmul01lt1lem2  46416  clim1fr1  46432  limcrecl  46460  climxrrelem  46578  liminflbuz2  46644  dvnprodlem1  46775  stoweidlem1  46830  stoweidlem11  46840  stoweidlem14  46843  stoweidlem24  46853  stoweidlem26  46855  wallispilem4  46897  wallispilem5  46898  stirlinglem1  46903  fourierdlem51  46986  fourierdlem65  47000  fouriersw  47060  2leaddle2  48187  2timesltsqm1  48268  sqrtpwpw2p  48442  lighneallem4a  48512  flnn0div2ge  49464  logbpw2m1  49498  functermclem  50434  amgmwlem  50821