Theorem eqbrtrrd 5094

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  dftpos4  8032  dif1en  8907  fodomfi  9022  resfifsupp  9086  cnfcom2lem  9389  ficardadju  9886  enfin1ai  10071  pwcfsdom  10270  fpwwe2lem6  10323  fpwwe2  10330  canthp1lem1  10339  1nqenq  10649  prlem936  10734  lemulge11  11767  supaddc  11872  supmul1  11874  mul2lt0llt0  12763  mul2lt0lgt0  12764  xaddge0  12921  xadddi2  12960  ltexp2a  13812  leexp2a  13818  nnlesq  13850  digit1  13880  faclbnd4lem1  13935  faclbnd6  13941  facavg  13943  prsshashgt1  14053  nehash2  14116  abs3dif  14971  abs2dif  14972  limsupgre  15118  rlimclim1  15182  rlimuni  15187  rlimres2  15198  rlimcn1  15225  rlimcn1b  15226  recn2  15238  imcn2  15239  rlimo1  15254  o1rlimmul  15256  iserex  15296  isercoll  15307  caucvgrlem2  15314  caucvgr  15315  iseraltlem3  15323  summolem2a  15355  fsumge1  15437  o1fsum  15453  isumrpcl  15483  climcnds  15491  harmonic  15499  mertenslem1  15524  prodmolem2a  15572  ege2le3  15727  efgt1p2  15751  efgt1p  15752  eirrlem  15841  rpnnen2lem11  15861  fsumdvds  15945  bitsfzo  16070  bitsmod  16071  bitscmp  16073  mulgcd  16184  dvdssqlem  16199  nn0seqcvgd  16203  mulgcddvds  16288  rpdvds  16293  qden1elz  16389  phimullem  16408  hashgcdlem  16417  hashgcdeq  16418  pcdvdstr  16505  pockthg  16535  prmreclem1  16545  4sqlem11  16584  ramub1lem1  16655  ramub1lem2  16656  mreexexlem4d  17273  sscid  17453  latmlej21  18113  latmlej22  18114  lubel  18147  efginvrel1  19249  odadd2  19365  odadd  19366  gexexlem  19368  cyggex2  19413  ablfacrplem  19583  ablfac1c  19589  ablfac1eu  19591  pgpfac1lem3a  19594  isabvd  19995  mptscmfsuppd  20104  znrrg  20685  frlmphl  20898  frlmup1  20915  f1linds  20942  chcoeffeqlem  21942  lmcn2  22708  metrtri  23418  imasdsf1olem  23434  stdbdxmet  23577  nrmmetd  23636  nmmtri  23684  nlmvscnlem2  23755  blcvx  23867  recld2  23883  zdis  23885  opnreen  23900  cnheibor  24024  lebnumlem3  24032  nmoleub2lem3  24184  nmoleub2lem2  24185  nmoleub3  24188  ipcnlem2  24313  cmetcaulem  24357  nglmle  24371  cncmet  24391  csbren  24468  trirn  24469  minveclem4  24501  ovoliunlem1  24571  ovoliun2  24575  ovolscalem1  24582  ovolicopnf  24593  voliunlem2  24620  volsup  24625  ioorcl2  24641  uniiccvol  24649  uniioombllem4  24655  i1fd  24750  mbfi1fseqlem4  24788  itg2const2  24811  itg2eqa  24815  itg2split  24819  itg2i1fseqle  24824  itg2cnlem2  24832  dvcnv  25046  dveflem  25048  dvferm1lem  25053  dvlip2  25064  c1liplem1  25065  dvivthlem1  25077  lhop1lem  25082  dvcvx  25089  dvfsumle  25090  dvfsumabs  25092  dvfsumlem4  25098  dvfsumrlim2  25101  ftc1a  25106  tdeglem4  25129  tdeglem4OLD  25130  deg1pwle  25189  fta1blem  25238  aalioulem3  25399  aaliou2b  25406  ulmbdd  25462  ulmdvlem1  25464  itgulm  25472  pserdvlem2  25492  abelthlem3  25497  abelthlem5  25499  abelthlem6  25500  abelthlem7  25502  tanregt0  25600  argimlt0  25673  logdivlti  25680  logcnlem3  25704  logcnlem4  25705  logtayl  25720  logtayl2  25722  cxple2  25757  cxpcn3lem  25805  cxpaddle  25810  isosctrlem1  25873  atantayl  25992  efrlim  26024  dfef2  26025  o1cxp  26029  cxp2lim  26031  divsqrtsumo1  26038  amgmlem  26044  logdifbnd  26048  emcllem7  26056  harmonicbnd4  26065  fsumharmonic  26066  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamucov  26092  lgamcvg2  26109  gamcvg2  26114  ftalem2  26128  basellem2  26136  basellem5  26139  basellem9  26143  vma1  26220  sqff1o  26236  fsumfldivdiaglem  26243  chtub  26265  fsumvma2  26267  chpchtsum  26272  chpub  26273  logfaclbnd  26275  logfacbnd3  26276  logfacrlim  26277  logexprlim  26278  bcmono  26330  bposlem2  26338  bposlem5  26341  bposlem6  26342  lgsne0  26388  lgsquadlem1  26433  lgsquadlem2  26434  2sqblem  26484  2sqmod  26489  chebbnd1lem1  26522  chtppilimlem1  26526  chtppilimlem2  26527  chpchtlim  26532  rplogsumlem1  26537  dchrvmasumiflem1  26554  dchrisum0flblem2  26562  dchrisum0fno1  26564  dchrisum0lem2a  26570  dchrisum0lem3  26572  dirith  26582  mulog2sumlem1  26587  mulog2sumlem2  26588  log2sumbnd  26597  selberglem2  26599  logdivbnd  26609  selberg3lem1  26610  selberg4lem1  26613  pntrsumbnd2  26620  pntrlog2bndlem1  26630  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntibndlem3  26645  pntlemb  26650  pntlemn  26653  pntlemr  26655  pntlemj  26656  pntlemf  26658  pntlemo  26660  ostth2lem3  26688  ostth3  26691  footeq  26989  hlperpnel  26990  perpdragALT  26992  perpdrag  26993  colperp  26994  mideulem2  26999  opphllem  27000  opphllem3  27014  lmieu  27049  trgcopy  27069  sacgr  27096  acopyeu  27099  usgredgleordALT  27504  eucrctshift  28508  nvabs  28935  smcnlem  28960  ubthlem2  29134  minvecolem4  29143  htthlem  29180  normpyc  29409  nmophmi  30294  hstle  30493  hstles  30494  stlei  30503  f1rnen  30865  fmptssfisupp  30921  nnmulge  30975  fsumiunle  31045  wrdt2ind  31127  xrge0npcan  31205  trsp2cyc  31292  archirngz  31345  archiabllem1a  31347  archiabllem2a  31350  archiabllem2c  31351  ornglmulle  31406  orngrmulle  31407  drngdimgt0  31603  lbsdiflsp0  31609  madjusmdetlem2  31680  esumpinfval  31941  esumpinfsum  31945  esumpcvgval  31946  esum2d  31961  esumiun  31962  dya2icoseg  32144  omssubadd  32167  carsgsigalem  32182  carsggect  32185  carsgclctunlem3  32187  omsmeas  32190  eulerpartlems  32227  sgnmulsgn  32416  signsplypnf  32429  signsply0  32430  reprlt  32499  reprinfz1  32502  hgt750lemc  32527  hgt750lemf  32533  pthhashvtx  32989  resconn  33108  sinccvglem  33530  circum  33532  dmttrcl  33707  ttrclselem2  33712  btwnxfr  34285  nn0prpwlem  34438  dnibndlem2  34586  unblimceq0  34614  irrdiff  35424  poimirlem7  35711  mblfinlem3  35743  mblfinlem4  35744  itg2addnclem3  35757  ftc1anc  35785  isbnd3  35869  cntotbnd  35881  bfp  35909  rrndstprj2  35916  1cvrjat  37416  3atlem1  37424  3atlem6  37429  llnmlplnN  37480  2llnjaN  37507  2lplnja  37560  dalem57  37670  dalawlem11  37822  dalawlem12  37823  lhp2lt  37942  lhpj1  37963  lhpm0atN  37970  4atexlemex2  38012  lautm  38035  cdleme17b  38228  cdleme20j  38259  cdleme30a  38319  cdlemg4c  38553  cdlemg17a  38602  cdlemg31c  38640  trljco  38681  cdlemk46  38889  dia2dimlem2  39006  cdlemm10N  39059  cdlemn10  39147  dihmeetlem1N  39231  dihglblem5apreN  39232  dihmeetlem15N  39262  mapdat  39608  lcmineqlem19  39983  lcmineqlem20  39984  aks4d1p1p5  40011  aks4d1p8d2  40021  aks4d1p8  40023  aks4d1p9  40024  metakunt29  40081  2xp3dxp2ge1d  40090  factwoffsmonot  40091  mhphflem  40207  dvdsexpnn  40261  rtprmirr  40268  fltnlta  40416  3cubeslem1  40422  irrapxlem1  40560  irrapxlem4  40563  pell1qrgaplem  40611  pellfundglb  40623  rmspecfund  40647  monotoddzzfi  40680  rmynn  40694  jm2.24nn  40697  jm2.17c  40700  jm2.24  40701  acongeq  40721  jm2.20nn  40735  jm2.26lem3  40739  jm2.27a  40743  jm2.27c  40745  rmydioph  40752  jm3.1lem2  40756  frlmpwfi  40839  areaquad  40963  rp-isfinite6  41023  frege129d  41260  leeq1d  41656  imo72b2  41672  cvgdvgrat  41820  radcnvrat  41821  hashnzfzclim  41829  isosctrlem1ALT  42443  cncmpmax  42464  iooabslt  42927  fmul01lt1lem2  43016  clim1fr1  43032  limcrecl  43060  climxrrelem  43180  liminflbuz2  43246  stoweidlem1  43432  stoweidlem11  43442  stoweidlem14  43445  stoweidlem24  43455  stoweidlem26  43457  wallispilem4  43499  wallispilem5  43500  stirlinglem1  43505  fourierdlem51  43588  fourierdlem65  43602  fouriersw  43662  2leaddle2  44678  sqrtpwpw2p  44878  lighneallem4a  44948  flnn0div2ge  45767  logbpw2m1  45801  amgmwlem  46392