Theorem eqbrtrrd 4607

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

Syntax hints:   → wi 4   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  dftpos4  7258  fodomfi  8124  resfifsupp  8186  cnfcom2lem  8481  infcda1  8898  enfin1ai  9089  fin56  9098  pwcfsdom  9284  fpwwe2lem7  9337  fpwwe2  9344  canthp1lem1  9353  1nqenq  9663  prlem936  9748  lemulge11  10764  supaddc  10867  supmul1  10869  mul2lt0llt0  11810  mul2lt0lgt0  11811  xaddge0  11960  xadddi2  11999  ltexp2a  12774  leexp2a  12778  nnlesq  12830  digit1  12860  faclbnd4lem1  12942  faclbnd6  12948  facavg  12950  prsshashgt1  13059  nehash2  13113  abs3dif  13919  abs2dif  13920  limsupgre  14060  rlimclim1  14124  rlimuni  14129  rlimres2  14140  rlimcn1  14167  rlimcn1b  14168  recn2  14179  imcn2  14180  rlimo1  14195  o1rlimmul  14197  iserex  14235  isercoll  14246  caucvgrlem2  14253  caucvgr  14254  iseraltlem3  14262  summolem2a  14293  fsumge1  14370  o1fsum  14386  isumrpcl  14414  climcnds  14422  harmonic  14430  mertenslem1  14455  prodmolem2a  14503  ege2le3  14659  efgt1p2  14683  efgt1p  14684  eirrlem  14771  rpnnen2lem11  14792  fsumdvds  14868  bitsfzo  14995  bitsmod  14996  bitscmp  14998  mulgcd  15103  dvdssqlem  15117  nn0seqcvgd  15121  mulgcddvds  15207  rpdvds  15212  qden1elz  15303  phimullem  15322  hashgcdlem  15331  hashgcdeq  15332  pcdvdstr  15418  pockthg  15448  prmreclem1  15458  4sqlem11  15497  ramub1lem1  15568  ramub1lem2  15569  mreexexlem4d  16130  sscid  16307  latmlej21  16915  latmlej22  16916  lubel  16945  efginvrel1  17964  odadd2  18075  odadd  18076  gexexlem  18078  cyggex2  18121  ablfacrplem  18287  ablfac1c  18293  ablfac1eu  18295  pgpfac1lem3a  18298  isabvd  18643  mptscmfsuppd  18752  znrrg  19733  frlmphl  19939  frlmup1  19956  f1linds  19983  chcoeffeqlem  20509  lmcn2  21262  metrtri  21972  imasdsf1olem  21988  stdbdxmet  22130  nrmmetd  22189  nmmtri  22236  nlmvscnlem2  22299  blcvx  22409  recld2  22425  zdis  22427  opnreen  22442  cnheibor  22562  lebnumlem3  22570  nmoleub2lem3  22723  nmoleub2lem2  22724  nmoleub3  22727  ipcnlem2  22851  cmetcaulem  22894  nglmle  22908  cncmet  22927  csbren  22990  trirn  22991  minveclem4  23011  ovoliunlem1  23077  ovoliun2  23081  ovolscalem1  23088  ovolicopnf  23099  voliunlem2  23126  volsup  23131  ioorcl2  23146  uniiccvol  23154  uniioombllem4  23160  i1fd  23254  mbfi1fseqlem4  23291  itg2const2  23314  itg2eqa  23318  itg2split  23322  itg2i1fseqle  23327  itg2cnlem2  23335  dvcnv  23544  dveflem  23546  dvferm1lem  23551  dvlip2  23562  c1liplem1  23563  dvivthlem1  23575  lhop1lem  23580  dvcvx  23587  dvfsumle  23588  dvfsumabs  23590  dvfsumlem4  23596  dvfsumrlim2  23599  ftc1a  23604  tdeglem4  23624  deg1pwle  23683  fta1blem  23732  aalioulem3  23893  aaliou2b  23900  ulmbdd  23956  ulmdvlem1  23958  itgulm  23966  pserdvlem2  23986  abelthlem3  23991  abelthlem5  23993  abelthlem6  23994  abelthlem7  23996  tanregt0  24089  argimlt0  24163  logdivlti  24170  logcnlem3  24190  logcnlem4  24191  logtayl  24206  logtayl2  24208  cxple2  24243  cxpcn3lem  24288  cxpaddle  24293  isosctrlem1  24348  atantayl  24464  efrlim  24496  dfef2  24497  o1cxp  24501  cxp2lim  24503  divsqrtsumo1  24510  amgmlem  24516  logdifbnd  24520  emcllem7  24528  harmonicbnd4  24537  fsumharmonic  24538  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamucov  24564  lgamcvg2  24581  gamcvg2  24586  ftalem2  24600  basellem2  24608  basellem5  24611  basellem9  24615  vma1  24692  sqff1o  24708  fsumfldivdiaglem  24715  chtub  24737  fsumvma2  24739  chpchtsum  24744  chpub  24745  logfaclbnd  24747  logfacbnd3  24748  logfacrlim  24749  logexprlim  24750  bcmono  24802  bposlem2  24810  bposlem5  24813  bposlem6  24814  lgsne0  24860  lgsquadlem1  24905  lgsquadlem2  24906  2sqblem  24956  chebbnd1lem1  24958  chtppilimlem1  24962  chtppilimlem2  24963  chpchtlim  24968  rplogsumlem1  24973  dchrvmasumiflem1  24990  dchrisum0flblem2  24998  dchrisum0fno1  25000  dchrisum0re  25002  dchrisum0lem2a  25006  dchrisum0lem3  25008  dirith  25018  mulog2sumlem1  25023  mulog2sumlem2  25024  log2sumbnd  25033  selberglem2  25035  logdivbnd  25045  selberg3lem1  25046  selberg4lem1  25049  pntrsumbnd2  25056  pntrlog2bndlem1  25066  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem3  25081  pntlemb  25086  pntlemn  25089  pntlemr  25091  pntlemj  25092  pntlemf  25094  pntlemo  25096  ostth2lem3  25124  ostth3  25127  footeq  25416  hlperpnel  25417  perpdragALT  25419  perpdrag  25420  colperp  25421  mideulem2  25426  opphllem  25427  opphllem3  25441  lmieu  25476  trgcopy  25496  sacgr  25522  acopyeu  25525  nvabs  26911  smcnlem  26936  ubthlem2  27111  minvecolem4  27120  htthlem  27158  normpyc  27387  nmophmi  28274  hstle  28473  hstles  28474  stlei  28483  2sqmod  28979  xrge0npcan  29025  archirngz  29074  archiabllem1a  29076  archiabllem2a  29079  archiabllem2c  29080  ornglmulle  29136  orngrmulle  29137  madjusmdetlem2  29222  esumpinfval  29462  esumpinfsum  29466  esumpcvgval  29467  esum2d  29482  esumiun  29483  dya2icoseg  29666  omssubadd  29689  carsgsigalem  29704  carsggect  29707  carsgclctunlem3  29709  omsmeas  29712  eulerpartlems  29749  sgnmulsgn  29938  signsplypnf  29953  signsply0  29954  rescon  30482  sinccvglem  30820  circum  30822  btwnxfr  31333  nn0prpwlem  31487  dnibndlem2  31639  poimirlem7  32586  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem3  32633  ftc1anc  32663  isbnd3  32753  cntotbnd  32765  bfp  32793  rrndstprj2  32800  1cvrjat  33779  3atlem1  33787  3atlem6  33792  llnmlplnN  33843  2llnjaN  33870  2lplnja  33923  dalem57  34033  dalawlem11  34185  dalawlem12  34186  lhp2lt  34305  lhpj1  34326  lhpm0atN  34333  4atexlemex2  34375  lautm  34398  cdleme17b  34592  cdleme20j  34624  cdleme30a  34684  cdlemg4c  34918  cdlemg17a  34967  cdlemg31c  35005  trljco  35046  cdlemk46  35254  dia2dimlem2  35372  cdlemm10N  35425  cdlemn10  35513  dihmeetlem1N  35597  dihglblem5apreN  35598  dihmeetlem15N  35628  mapdat  35974  irrapxlem1  36404  irrapxlem4  36407  pell1qrgaplem  36455  pellfundglb  36467  rmspecfund  36492  monotoddzzfi  36525  rmynn  36541  jm2.24nn  36544  jm2.17c  36547  jm2.24  36548  acongeq  36568  jm2.20nn  36582  jm2.26lem3  36586  jm2.27a  36590  jm2.27c  36592  rmydioph  36599  jm3.1lem2  36603  frlmpwfi  36686  areaquad  36821  rp-isfinite6  36883  frege129d  37074  imo72b2  37497  cvgdvgrat  37534  radcnvrat  37535  hashnzfzclim  37543  isosctrlem1ALT  38192  cncmpmax  38214  iooabslt  38568  fmul01lt1lem2  38652  clim1fr1  38668  limcrecl  38696  stoweidlem1  38894  stoweidlem11  38904  stoweidlem14  38907  stoweidlem24  38917  stoweidlem26  38919  wallispilem4  38961  wallispilem5  38962  stirlinglem1  38967  fourierdlem51  39050  fourierdlem65  39064  fouriersw  39124  sqrtpwpw2p  39988  lighneallem4a  40063  2leaddle2  40344  usgredgaleordALT  40461  eucrctshift  41411  flnn0div2ge  42121  logbpw2m1  42159  amgmwlem  42357