Theorem eqbrtrrd 4912

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 2784	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 4910	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1601   class class class wbr 4888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4889

This theorem is referenced by:  dftpos4  7655  fodomfi  8529  resfifsupp  8593  cnfcom2lem  8897  infcda1  9352  enfin1ai  9543  fin56  9552  pwcfsdom  9742  fpwwe2lem7  9795  fpwwe2  9802  canthp1lem1  9811  1nqenq  10121  prlem936  10206  lemulge11  11241  supaddc  11348  supmul1  11350  mul2lt0llt0  12247  mul2lt0lgt0  12248  xaddge0  12404  xadddi2  12443  ltexp2a  13234  leexp2a  13238  nnlesq  13291  digit1  13321  faclbnd4lem1  13402  faclbnd6  13408  facavg  13410  prsshashgt1  13516  nehash2  13574  abs3dif  14482  abs2dif  14483  limsupgre  14624  rlimclim1  14688  rlimuni  14693  rlimres2  14704  rlimcn1  14731  rlimcn1b  14732  recn2  14743  imcn2  14744  rlimo1  14759  o1rlimmul  14761  iserex  14799  isercoll  14810  caucvgrlem2  14817  caucvgr  14818  iseraltlem3  14826  summolem2a  14857  fsumge1  14937  o1fsum  14953  isumrpcl  14983  climcnds  14991  harmonic  14999  mertenslem1  15023  prodmolem2a  15071  ege2le3  15226  efgt1p2  15250  efgt1p  15251  eirrlem  15340  rpnnen2lem11  15361  fsumdvds  15441  bitsfzo  15567  bitsmod  15568  bitscmp  15570  mulgcd  15675  dvdssqlem  15689  nn0seqcvgd  15693  mulgcddvds  15778  rpdvds  15783  qden1elz  15873  phimullem  15892  hashgcdlem  15901  hashgcdeq  15902  pcdvdstr  15988  pockthg  16018  prmreclem1  16028  4sqlem11  16067  ramub1lem1  16138  ramub1lem2  16139  mreexexlem4d  16697  sscid  16873  latmlej21  17482  latmlej22  17483  lubel  17512  efginvrel1  18529  odadd2  18642  odadd  18643  gexexlem  18645  cyggex2  18688  ablfacrplem  18855  ablfac1c  18861  ablfac1eu  18863  pgpfac1lem3a  18866  isabvd  19216  mptscmfsuppd  19325  znrrg  20313  frlmphl  20528  frlmup1  20545  f1linds  20572  chcoeffeqlem  21101  lmcn2  21865  metrtri  22574  imasdsf1olem  22590  stdbdxmet  22732  nrmmetd  22791  nmmtri  22838  nlmvscnlem2  22901  blcvx  23013  recld2  23029  zdis  23031  opnreen  23046  cnheibor  23166  lebnumlem3  23174  nmoleub2lem3  23326  nmoleub2lem2  23327  nmoleub3  23330  ipcnlem2  23454  cmetcaulem  23498  nglmle  23512  cncmet  23532  csbren  23609  trirn  23610  minveclem4  23642  ovoliunlem1  23710  ovoliun2  23714  ovolscalem1  23721  ovolicopnf  23732  voliunlem2  23759  volsup  23764  ioorcl2  23780  uniiccvol  23788  uniioombllem4  23794  i1fd  23889  mbfi1fseqlem4  23926  itg2const2  23949  itg2eqa  23953  itg2split  23957  itg2i1fseqle  23962  itg2cnlem2  23970  dvcnv  24181  dveflem  24183  dvferm1lem  24188  dvlip2  24199  c1liplem1  24200  dvivthlem1  24212  lhop1lem  24217  dvcvx  24224  dvfsumle  24225  dvfsumabs  24227  dvfsumlem4  24233  dvfsumrlim2  24236  ftc1a  24241  tdeglem4  24261  deg1pwle  24320  fta1blem  24369  aalioulem3  24530  aaliou2b  24537  ulmbdd  24593  ulmdvlem1  24595  itgulm  24603  pserdvlem2  24623  abelthlem3  24628  abelthlem5  24630  abelthlem6  24631  abelthlem7  24633  tanregt0  24727  argimlt0  24800  logdivlti  24807  logcnlem3  24831  logcnlem4  24832  logtayl  24847  logtayl2  24849  cxple2  24884  cxpcn3lem  24932  cxpaddle  24937  isosctrlem1  25000  atantayl  25119  efrlim  25152  dfef2  25153  o1cxp  25157  cxp2lim  25159  divsqrtsumo1  25166  amgmlem  25172  logdifbnd  25176  emcllem7  25184  harmonicbnd4  25193  fsumharmonic  25194  lgamgulmlem2  25212  lgamgulmlem3  25213  lgamucov  25220  lgamcvg2  25237  gamcvg2  25242  ftalem2  25256  basellem2  25264  basellem5  25267  basellem9  25271  vma1  25348  sqff1o  25364  fsumfldivdiaglem  25371  chtub  25393  fsumvma2  25395  chpchtsum  25400  chpub  25401  logfaclbnd  25403  logfacbnd3  25404  logfacrlim  25405  logexprlim  25406  bcmono  25458  bposlem2  25466  bposlem5  25469  bposlem6  25470  lgsne0  25516  lgsquadlem1  25561  lgsquadlem2  25562  2sqblem  25612  chebbnd1lem1  25614  chtppilimlem1  25618  chtppilimlem2  25619  chpchtlim  25624  rplogsumlem1  25629  dchrvmasumiflem1  25646  dchrisum0flblem2  25654  dchrisum0fno1  25656  dchrisum0re  25658  dchrisum0lem2a  25662  dchrisum0lem3  25664  dirith  25674  mulog2sumlem1  25679  mulog2sumlem2  25680  log2sumbnd  25689  selberglem2  25691  logdivbnd  25701  selberg3lem1  25702  selberg4lem1  25705  pntrsumbnd2  25712  pntrlog2bndlem1  25722  pntrlog2bndlem5  25726  pntrlog2bndlem6  25728  pntpbnd1a  25730  pntpbnd1  25731  pntpbnd2  25732  pntibndlem3  25737  pntlemb  25742  pntlemn  25745  pntlemr  25747  pntlemj  25748  pntlemf  25750  pntlemo  25752  ostth2lem3  25780  ostth3  25783  footeq  26076  hlperpnel  26077  perpdragALT  26079  perpdrag  26080  colperp  26081  mideulem2  26086  opphllem  26087  opphllem3  26101  lmieu  26136  trgcopy  26156  sacgr  26183  sacgrOLD  26184  acopyeu  26187  usgredgleordALT  26585  eucrctshift  27651  nvabs  28103  smcnlem  28128  ubthlem2  28303  minvecolem4  28312  htthlem  28350  normpyc  28579  nmophmi  29466  hstle  29665  hstles  29666  stlei  29675  nnmulge  30084  fsumiunle  30143  2sqmod  30214  xrge0npcan  30260  archirngz  30309  archiabllem1a  30311  archiabllem2a  30314  archiabllem2c  30315  ornglmulle  30371  orngrmulle  30372  lbsdiflsp0  30444  madjusmdetlem2  30496  esumpinfval  30737  esumpinfsum  30741  esumpcvgval  30742  esum2d  30757  esumiun  30758  dya2icoseg  30941  omssubadd  30964  carsgsigalem  30979  carsggect  30982  carsgclctunlem3  30984  omsmeas  30987  eulerpartlems  31024  sgnmulsgn  31214  signsplypnf  31231  signsply0  31232  reprlt  31303  reprinfz1  31306  hgt750lemc  31331  hgt750lemf  31337  resconn  31831  sinccvglem  32167  circum  32169  btwnxfr  32756  nn0prpwlem  32909  dnibndlem2  33056  poimirlem7  34047  mblfinlem3  34079  mblfinlem4  34080  itg2addnclem3  34093  ftc1anc  34123  isbnd3  34212  cntotbnd  34224  bfp  34252  rrndstprj2  34259  1cvrjat  35634  3atlem1  35642  3atlem6  35647  llnmlplnN  35698  2llnjaN  35725  2lplnja  35778  dalem57  35888  dalawlem11  36040  dalawlem12  36041  lhp2lt  36160  lhpj1  36181  lhpm0atN  36188  4atexlemex2  36230  lautm  36253  cdleme17b  36446  cdleme20j  36477  cdleme30a  36537  cdlemg4c  36771  cdlemg17a  36820  cdlemg31c  36858  trljco  36899  cdlemk46  37107  dia2dimlem2  37224  cdlemm10N  37277  cdlemn10  37365  dihmeetlem1N  37449  dihglblem5apreN  37450  dihmeetlem15N  37480  mapdat  37826  rtprmirr  38178  irrapxlem1  38356  irrapxlem4  38359  pell1qrgaplem  38407  pellfundglb  38419  rmspecfund  38443  monotoddzzfi  38476  rmynn  38492  jm2.24nn  38495  jm2.17c  38498  jm2.24  38499  acongeq  38519  jm2.20nn  38533  jm2.26lem3  38537  jm2.27a  38541  jm2.27c  38543  rmydioph  38550  jm3.1lem2  38554  frlmpwfi  38637  areaquad  38770  rp-isfinite6  38831  frege129d  39022  leeq1d  39421  imo72b2  39441  cvgdvgrat  39478  radcnvrat  39479  hashnzfzclim  39487  isosctrlem1ALT  40113  cncmpmax  40134  iooabslt  40643  fmul01lt1lem2  40735  clim1fr1  40751  limcrecl  40779  climxrrelem  40899  liminflbuz2  40965  stoweidlem1  41155  stoweidlem11  41165  stoweidlem14  41168  stoweidlem24  41178  stoweidlem26  41180  wallispilem4  41222  wallispilem5  41223  stirlinglem1  41228  fourierdlem51  41311  fourierdlem65  41325  fouriersw  41385  2leaddle2  42350  sqrtpwpw2p  42481  lighneallem4a  42556  flnn0div2ge  43352  logbpw2m1  43386  amgmwlem  43664