Theorem eqbrtrrd 5126

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  dftpos4  8201  dif1en  9101  dif1enOLD  9103  fodomfi  9237  fodomfiOLD  9257  fmptssfisupp  9321  resfifsupp  9324  cnfcom2lem  9630  dmttrcl  9650  ttrclselem2  9655  ficardadju  10129  enfin1ai  10313  pwcfsdom  10512  fpwwe2lem6  10565  fpwwe2  10572  canthp1lem1  10581  1nqenq  10891  prlem936  10976  lemulge11  12021  supaddc  12126  supmul1  12128  mul2lt0llt0  13033  mul2lt0lgt0  13034  xaddge0  13194  xadddi2  13233  ltexp2a  14107  leexp2a  14113  nnlesq  14146  digit1  14178  faclbnd4lem1  14234  faclbnd6  14240  facavg  14242  prsshashgt1  14351  nehash2  14415  abs3dif  15274  abs2dif  15275  limsupgre  15423  rlimclim1  15487  rlimuni  15492  rlimres2  15503  rlimcn1  15530  rlimcn1b  15531  recn2  15543  imcn2  15544  rlimo1  15559  o1rlimmul  15561  iserex  15599  isercoll  15610  caucvgrlem2  15617  caucvgr  15618  iseraltlem3  15626  summolem2a  15657  fsumge1  15739  o1fsum  15755  isumrpcl  15785  climcnds  15793  harmonic  15801  mertenslem1  15826  prodmolem2a  15876  ege2le3  16032  efgt1p2  16058  efgt1p  16059  eirrlem  16148  rpnnen2lem11  16168  fsumdvds  16254  bitsfzo  16381  bitsmod  16382  bitscmp  16384  mulgcd  16494  dvdssqlem  16512  nn0seqcvgd  16516  mulgcddvds  16601  rpdvds  16606  qden1elz  16703  phimullem  16725  hashgcdlem  16734  hashgcdeq  16736  pcdvdstr  16823  pockthg  16853  prmreclem1  16863  4sqlem11  16902  ramub1lem1  16973  ramub1lem2  16974  mreexexlem4d  17588  sscid  17766  latmlej21  18421  latmlej22  18422  lubel  18455  efginvrel1  19642  odadd2  19763  odadd  19764  gexexlem  19766  cyggex2  19811  ablfacrplem  19981  ablfac1c  19987  ablfac1eu  19989  pgpfac1lem3a  19992  isabvd  20732  ornglmulle  20787  orngrmulle  20788  mptscmfsuppd  20866  znrrg  21507  frlmphl  21723  frlmup1  21740  f1linds  21767  psdmplcl  22082  chcoeffeqlem  22805  lmcn2  23569  metrtri  24278  imasdsf1olem  24294  stdbdxmet  24436  nrmmetd  24495  nmmtri  24543  nlmvscnlem2  24606  blcvx  24719  recld2  24736  zdis  24738  opnreen  24753  cnheibor  24887  lebnumlem3  24895  nmoleub2lem3  25048  nmoleub2lem2  25049  nmoleub3  25052  ipcnlem2  25177  cmetcaulem  25221  nglmle  25235  cncmet  25255  csbren  25332  trirn  25333  minveclem4  25365  ovoliunlem1  25436  ovoliun2  25440  ovolscalem1  25447  ovolicopnf  25458  voliunlem2  25485  volsup  25490  ioorcl2  25506  uniiccvol  25514  uniioombllem4  25520  i1fd  25615  mbfi1fseqlem4  25652  itg2const2  25675  itg2eqa  25679  itg2split  25683  itg2i1fseqle  25688  itg2cnlem2  25696  dvcnv  25914  dveflem  25916  dvferm1lem  25921  dvlip2  25933  c1liplem1  25934  dvivthlem1  25946  lhop1lem  25951  dvcvx  25958  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  dvfsumlem4  25969  dvfsumrlim2  25972  ftc1a  25977  tdeglem4  25998  deg1pwle  26058  fta1blem  26109  aalioulem3  26275  aaliou2b  26282  ulmbdd  26340  ulmdvlem1  26342  itgulm  26350  pserdvlem2  26371  abelthlem3  26376  abelthlem5  26378  abelthlem6  26379  abelthlem7  26381  tanregt0  26481  argimlt0  26555  logdivlti  26562  logcnlem3  26586  logcnlem4  26587  logtayl  26602  logtayl2  26604  cxple2  26639  cxpcn3lem  26690  cxpaddle  26695  rtprmirr  26703  isosctrlem1  26761  atantayl  26880  efrlim  26912  efrlimOLD  26913  dfef2  26914  o1cxp  26918  cxp2lim  26920  divsqrtsumo1  26927  amgmlem  26933  logdifbnd  26937  emcllem7  26945  harmonicbnd4  26954  fsumharmonic  26955  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamucov  26981  lgamcvg2  26998  gamcvg2  27003  ftalem2  27017  basellem2  27025  basellem5  27028  basellem9  27032  vma1  27109  sqff1o  27125  fsumfldivdiaglem  27132  chtub  27156  fsumvma2  27158  chpchtsum  27163  chpub  27164  logfaclbnd  27166  logfacbnd3  27167  logfacrlim  27168  logexprlim  27169  bcmono  27221  bposlem2  27229  bposlem5  27232  bposlem6  27233  lgsne0  27279  lgsquadlem1  27324  lgsquadlem2  27325  2sqblem  27375  2sqmod  27380  chebbnd1lem1  27413  chtppilimlem1  27417  chtppilimlem2  27418  chpchtlim  27423  rplogsumlem1  27428  dchrvmasumiflem1  27445  dchrisum0flblem2  27453  dchrisum0fno1  27455  dchrisum0lem2a  27461  dchrisum0lem3  27463  dirith  27473  mulog2sumlem1  27478  mulog2sumlem2  27479  log2sumbnd  27488  selberglem2  27490  logdivbnd  27500  selberg3lem1  27501  selberg4lem1  27504  pntrsumbnd2  27511  pntrlog2bndlem1  27521  pntrlog2bndlem5  27525  pntrlog2bndlem6  27527  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  pntibndlem3  27536  pntlemb  27541  pntlemn  27544  pntlemr  27546  pntlemj  27547  pntlemf  27549  pntlemo  27551  ostth2lem3  27579  ostth3  27582  addsuniflem  27948  sltp1d  27962  negsid  27987  negsunif  28001  mulsuniflem  28092  precsexlem9  28157  n0sge0  28270  zscut  28335  halfcut  28381  addhalfcut  28382  footeq  28704  hlperpnel  28705  perpdragALT  28707  perpdrag  28708  colperp  28709  mideulem2  28714  opphllem  28715  opphllem3  28729  lmieu  28764  trgcopy  28784  sacgr  28811  acopyeu  28814  usgredgleordALT  29214  eucrctshift  30222  nvabs  30651  smcnlem  30676  ubthlem2  30850  minvecolem4  30859  htthlem  30896  normpyc  31125  nmophmi  32010  hstle  32209  hstles  32210  stlei  32219  f1rnen  32603  nnmulge  32712  fsumiunle  32804  sgnmulsgn  32817  wrdt2ind  32925  xrge0npcan  33004  gsumwrd2dccat  33050  trsp2cyc  33095  archirngz  33158  archiabllem1a  33160  archiabllem2a  33163  archiabllem2c  33164  elrgspnlem1  33209  elrgspn  33213  elrgspnsubrunlem2  33215  rprmasso  33489  q1pdir  33561  r1pquslmic  33569  drngdimgt0  33607  lbsdiflsp0  33615  fldextrspundgle  33666  fldext2rspun  33670  minplyirredlem  33693  madjusmdetlem2  33811  esumpinfval  34056  esumpinfsum  34060  esumpcvgval  34061  esum2d  34076  esumiun  34077  dya2icoseg  34261  omssubadd  34284  carsgsigalem  34299  carsggect  34302  carsgclctunlem3  34304  omsmeas  34307  eulerpartlems  34344  signsplypnf  34534  signsply0  34535  reprlt  34603  reprinfz1  34606  hgt750lemc  34631  hgt750lemf  34637  pthhashvtx  35108  resconn  35226  sinccvglem  35652  circum  35654  btwnxfr  36037  nn0prpwlem  36303  dnibndlem2  36460  unblimceq0  36488  irrdiff  37307  poimirlem7  37614  mblfinlem3  37646  mblfinlem4  37647  itg2addnclem3  37660  ftc1anc  37688  isbnd3  37771  cntotbnd  37783  bfp  37811  rrndstprj2  37818  1cvrjat  39462  3atlem1  39470  3atlem6  39475  llnmlplnN  39526  2llnjaN  39553  2lplnja  39606  dalem57  39716  dalawlem11  39868  dalawlem12  39869  lhp2lt  39988  lhpj1  40009  lhpm0atN  40016  4atexlemex2  40058  lautm  40081  cdleme17b  40274  cdleme20j  40305  cdleme30a  40365  cdlemg4c  40599  cdlemg17a  40648  cdlemg31c  40686  trljco  40727  cdlemk46  40935  dia2dimlem2  41052  cdlemm10N  41105  cdlemn10  41193  dihmeetlem1N  41277  dihglblem5apreN  41278  dihmeetlem15N  41308  mapdat  41654  lcmineqlem19  42028  lcmineqlem20  42029  aks4d1p1p5  42056  aks4d1p8d2  42066  aks4d1p8  42068  aks4d1p9  42069  hashscontpow  42103  dvdsexpnn  42314  mullt0b1d  42464  selvvvval  42566  evlselv  42568  mhphflem  42577  fltnlta  42644  3cubeslem1  42665  irrapxlem1  42803  irrapxlem4  42806  pell1qrgaplem  42854  pellfundglb  42866  rmspecfund  42890  monotoddzzfi  42924  rmynn  42938  jm2.24nn  42941  jm2.17c  42944  jm2.24  42945  acongeq  42965  jm2.20nn  42979  jm2.26lem3  42983  jm2.27a  42987  jm2.27c  42989  rmydioph  42996  jm3.1lem2  43000  frlmpwfi  43080  areaquad  43198  cantnf2  43307  rp-isfinite6  43500  frege129d  43745  leeq1d  44139  imo72b2lem0  44147  imo72b2  44154  cvgdvgrat  44295  radcnvrat  44296  hashnzfzclim  44304  isosctrlem1ALT  44916  cncmpmax  45019  iooabslt  45490  fmul01lt1lem2  45576  clim1fr1  45592  limcrecl  45620  climxrrelem  45740  liminflbuz2  45806  dvnprodlem1  45937  stoweidlem1  45992  stoweidlem11  46002  stoweidlem14  46005  stoweidlem24  46015  stoweidlem26  46017  wallispilem4  46059  wallispilem5  46060  stirlinglem1  46065  fourierdlem51  46148  fourierdlem65  46162  fouriersw  46222  2leaddle2  47292  sqrtpwpw2p  47532  lighneallem4a  47602  flnn0div2ge  48515  logbpw2m1  48549  functermclem  49489  amgmwlem  49784