Theorem eqbrtrrd 5139

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

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  dftpos4  8241  dif1en  9146  fodomfi  9272  fmptssfisupp  9354  cnfcom2lem  9670  dmttrcl  9690  ttrclselem2  9695  ficardadju  10183  enfin1ai  10368  pwcfsdom  10568  fpwwe2lem6  10621  fpwwe2  10628  canthp1lem1  10637  1nqenq  10947  prlem936  11032  lemulge11  12077  supaddc  12182  supmul1  12184  mul2lt0llt0  13122  mul2lt0lgt0  13123  xaddge0  13284  xadddi2  13323  ltexp2a  14202  leexp2a  14208  nnlesq  14241  digit1  14273  faclbnd4lem1  14329  faclbnd6  14335  facavg  14337  prsshashgt1  14447  nehash2  14511  sgnmulsgn  15146  abs3dif  15383  abs2dif  15384  limsupgre  15532  rlimclim1  15596  rlimuni  15601  rlimres2  15612  rlimcn1  15639  rlimcn1b  15640  recn2  15652  imcn2  15653  rlimo1  15668  o1rlimmul  15670  iserex  15708  isercoll  15719  caucvgrlem2  15726  caucvgr  15727  iseraltlem3  15735  summolem2a  15766  fsumge1  15849  o1fsum  15865  isumrpcl  15897  climcnds  15905  harmonic  15913  mertenslem1  15938  prodmolem2a  15988  ege2le3  16144  efgt1p2  16170  efgt1p  16171  eirrlem  16260  rpnnen2lem11  16280  fsumdvds  16366  bitsfzo  16493  bitsmod  16494  bitscmp  16496  mulgcd  16606  dvdssqlem  16624  nn0seqcvgd  16628  mulgcddvds  16713  rpdvds  16718  qden1elz  16816  phimullem  16838  hashgcdlem  16847  hashgcdeq  16849  pcdvdstr  16936  pockthg  16966  prmreclem1  16976  4sqlem11  17015  ramub1lem1  17086  ramub1lem2  17087  mreexexlem4d  17703  sscid  17881  latmlej21  18536  latmlej22  18537  lubel  18570  efginvrel1  19798  odadd2  19919  odadd  19920  gexexlem  19922  cyggex2  19967  ablfacrplem  20137  ablfac1c  20143  ablfac1eu  20145  pgpfac1lem3a  20148  isabvd  20893  ornglmulle  20948  orngrmulle  20949  mptscmfsuppd  21027  znrrg  21684  frlmphl  21900  frlmup1  21917  f1linds  21944  selvvvval  22262  psdmplcl  22294  chcoeffeqlem  23011  lmcn2  23775  metrtri  24483  imasdsf1olem  24499  stdbdxmet  24641  nrmmetd  24700  nmmtri  24748  nlmvscnlem2  24811  blcvx  24924  recld2  24941  zdis  24943  opnreen  24958  cnheibor  25083  lebnumlem3  25091  nmoleub2lem3  25243  nmoleub2lem2  25244  nmoleub3  25247  ipcnlem2  25372  cmetcaulem  25416  nglmle  25430  cncmet  25450  csbren  25527  trirn  25528  minveclem4  25560  ovoliunlem1  25630  ovoliun2  25634  ovolscalem1  25641  ovolicopnf  25652  voliunlem2  25679  volsup  25684  ioorcl2  25700  uniiccvol  25708  uniioombllem4  25714  i1fd  25809  mbfi1fseqlem4  25846  itg2const2  25869  itg2eqa  25873  itg2split  25877  itg2i1fseqle  25882  itg2cnlem2  25890  dvcnv  26105  dveflem  26107  dvferm1lem  26112  dvlip2  26123  c1liplem1  26124  dvivthlem1  26136  lhop1lem  26141  dvcvx  26148  dvfsumle  26149  dvfsumabs  26151  dvfsumlem4  26157  dvfsumrlim2  26160  ftc1a  26165  tdeglem4  26186  deg1pwle  26246  fta1blem  26297  aalioulem3  26464  aaliou2b  26471  ulmbdd  26527  ulmdvlem1  26529  itgulm  26537  pserdvlem2  26557  abelthlem3  26562  abelthlem5  26564  abelthlem6  26565  abelthlem7  26567  tanregt0  26670  argimlt0  26744  logdivlti  26751  logcnlem3  26775  logcnlem4  26776  logtayl  26791  logtayl2  26793  cxple2  26828  cxpcn3lem  26878  cxpaddle  26883  rtprmirr  26891  isosctrlem1  26949  atantayl  27068  efrlim  27100  dfef2  27101  o1cxp  27105  cxp2lim  27107  divsqrtsumo1  27114  amgmlem  27120  logdifbnd  27124  emcllem7  27132  harmonicbnd4  27141  fsumharmonic  27142  lgamgulmlem2  27160  lgamgulmlem3  27161  lgamucov  27168  lgamcvg2  27185  gamcvg2  27190  ftalem2  27204  basellem2  27212  basellem5  27215  basellem9  27219  vma1  27296  sqff1o  27312  fsumfldivdiaglem  27319  chtub  27342  fsumvma2  27344  chpchtsum  27349  chpub  27350  logfaclbnd  27352  logfacbnd3  27353  logfacrlim  27354  logexprlim  27355  bcmono  27407  bposlem2  27415  bposlem5  27418  bposlem6  27419  lgsne0  27465  lgsquadlem1  27510  lgsquadlem2  27511  2sqblem  27561  2sqmod  27566  chebbnd1lem1  27599  chtppilimlem1  27603  chtppilimlem2  27604  chpchtlim  27609  rplogsumlem1  27614  dchrvmasumiflem1  27631  dchrisum0flblem2  27639  dchrisum0fno1  27641  dchrisum0lem2a  27647  dchrisum0lem3  27649  dirith  27659  mulog2sumlem1  27664  mulog2sumlem2  27665  log2sumbnd  27674  selberglem2  27676  logdivbnd  27686  selberg3lem1  27687  selberg4lem1  27690  pntrsumbnd2  27697  pntrlog2bndlem1  27707  pntrlog2bndlem5  27711  pntrlog2bndlem6  27713  pntpbnd1a  27715  pntpbnd1  27716  pntpbnd2  27717  pntibndlem3  27722  pntlemb  27727  pntlemn  27730  pntlemr  27732  pntlemj  27733  pntlemf  27735  pntlemo  27737  ostth2lem3  27765  ostth3  27768  addsuniflem  28160  ltsp1d  28174  negsid  28200  negsunif  28214  negleft  28217  mulsuniflem  28308  precsexlem9  28374  n0sge0  28497  zcuts  28566  halfcut  28617  addhalfcut  28618  pw2cut2  28621  bdayfinbndlem1  28626  footeq  28963  hlperpnel  28965  perpdragALT  28967  perpdrag  28968  colperp  28969  mideulem2  28974  opphllem  28975  opphllem3  28989  lmieu  29051  trgcopy  29072  sacgr  29099  acopyeu  29102  perpeqlem  29105  perpprlng  29153  usgredgleordALT  29525  eucrctshift  30535  nvabs  30965  smcnlem  30990  ubthlem2  31164  minvecolem4  31173  htthlem  31210  normpyc  31439  nmophmi  32324  hstle  32523  hstles  32524  stlei  32533  f1rnen  32914  nnmulge  33025  fsumiunle  33114  wrdt2ind  33214  xrge0npcan  33281  gsumwrd2dccat  33339  trsp2cyc  33384  archirngz  33450  archiabllem1a  33452  archiabllem2a  33455  archiabllem2c  33456  elrgspnlem1  33503  elrgspn  33507  elrgspnsubrunlem2  33509  rprmasso  33760  q1pdir  33838  r1pquslmic  33845  selvply1rhmlema  33853  selvply1rhmlem1  33855  evlextv  33877  mplvrpmga  33880  mplvrpmrhm  33882  drngdimgt0  33953  lbsdiflsp0  33961  fldextrspundgle  34013  fldext2rspun  34017  minplyirredlem  34045  madjusmdetlem2  34163  esumpinfval  34408  esumpinfsum  34412  esumpcvgval  34413  esum2d  34428  esumiun  34429  dya2icoseg  34612  omssubadd  34635  carsgsigalem  34650  carsggect  34653  carsgclctunlem3  34655  omsmeas  34658  eulerpartlems  34695  signsplypnf  34882  signsply0  34883  reprlt  34951  reprinfz1  34954  hgt750lemc  34979  hgt750lemf  34985  pthhashvtx  35519  resconn  35637  sinccvglem  36063  circum  36065  btwnxfr  36447  nn0prpwlem  36722  dnibndlem2  36957  unblimceq0  36985  irrdiff  37858  poimirlem7  38166  mblfinlem3  38198  mblfinlem4  38199  itg2addnclem3  38212  ftc1anc  38240  isbnd3  38323  cntotbnd  38335  bfp  38363  rrndstprj2  38370  1cvrjat  40139  3atlem1  40147  3atlem6  40152  llnmlplnN  40203  2llnjaN  40230  2lplnja  40283  dalem57  40393  dalawlem11  40545  dalawlem12  40546  lhp2lt  40665  lhpj1  40686  lhpm0atN  40693  4atexlemex2  40735  lautm  40758  cdleme17b  40951  cdleme20j  40982  cdleme30a  41042  cdlemg4c  41276  cdlemg17a  41325  cdlemg31c  41363  trljco  41404  cdlemk46  41612  dia2dimlem2  41729  cdlemm10N  41782  cdlemn10  41870  dihmeetlem1N  41954  dihglblem5apreN  41955  dihmeetlem15N  41985  mapdat  42331  lcmineqlem19  42704  lcmineqlem20  42705  aks4d1p1p5  42732  aks4d1p8d2  42742  aks4d1p8  42744  aks4d1p9  42745  hashscontpow  42779  dvdsexpnn  42984  mullt0b1d  43147  evlselv  43213  mhphflem  43220  fltnlta  43287  3cubeslem1  43307  irrapxlem1  43441  irrapxlem4  43444  pell1qrgaplem  43492  pellfundglb  43504  rmspecfund  43528  monotoddzzfi  43561  rmynn  43575  jm2.24nn  43578  jm2.17c  43581  jm2.24  43582  acongeq  43602  jm2.20nn  43616  jm2.26lem3  43620  jm2.27a  43624  jm2.27c  43626  rmydioph  43633  jm3.1lem2  43637  frlmpwfi  43717  areaquad  43835  cantnf2  43944  rp-isfinite6  44136  frege129d  44381  leeq1d  44775  imo72b2lem0  44783  imo72b2  44790  cvgdvgrat  44915  radcnvrat  44916  hashnzfzclim  44924  isosctrlem1ALT  45534  cncmpmax  45644  iooabslt  46107  fmul01lt1lem2  46193  clim1fr1  46209  limcrecl  46237  climxrrelem  46355  liminflbuz2  46421  dvnprodlem1  46552  stoweidlem1  46607  stoweidlem11  46617  stoweidlem14  46620  stoweidlem24  46630  stoweidlem26  46632  wallispilem4  46674  wallispilem5  46675  stirlinglem1  46680  fourierdlem51  46763  fourierdlem65  46777  fouriersw  46837  2leaddle2  47924  2timesltsqm1  48005  sqrtpwpw2p  48179  lighneallem4a  48249  flnn0div2ge  49198  logbpw2m1  49232  functermclem  50170  amgmwlem  50476