Theorem eqbrtrrd 4677

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

Syntax hints:   → wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  dftpos4  7371  fodomfi  8239  resfifsupp  8303  cnfcom2lem  8598  infcda1  9015  enfin1ai  9206  fin56  9215  pwcfsdom  9405  fpwwe2lem7  9458  fpwwe2  9465  canthp1lem1  9474  1nqenq  9784  prlem936  9869  lemulge11  10885  supaddc  10990  supmul1  10992  mul2lt0llt0  11934  mul2lt0lgt0  11935  xaddge0  12088  xadddi2  12127  ltexp2a  12912  leexp2a  12916  nnlesq  12968  digit1  12998  faclbnd4lem1  13080  faclbnd6  13086  facavg  13088  prsshashgt1  13198  nehash2  13256  abs3dif  14071  abs2dif  14072  limsupgre  14212  rlimclim1  14276  rlimuni  14281  rlimres2  14292  rlimcn1  14319  rlimcn1b  14320  recn2  14331  imcn2  14332  rlimo1  14347  o1rlimmul  14349  iserex  14387  isercoll  14398  caucvgrlem2  14405  caucvgr  14406  iseraltlem3  14414  summolem2a  14446  fsumge1  14529  o1fsum  14545  isumrpcl  14575  climcnds  14583  harmonic  14591  mertenslem1  14616  prodmolem2a  14664  ege2le3  14820  efgt1p2  14844  efgt1p  14845  eirrlem  14932  rpnnen2lem11  14953  fsumdvds  15030  bitsfzo  15157  bitsmod  15158  bitscmp  15160  mulgcd  15265  dvdssqlem  15279  nn0seqcvgd  15283  mulgcddvds  15369  rpdvds  15374  qden1elz  15465  phimullem  15484  hashgcdlem  15493  hashgcdeq  15494  pcdvdstr  15580  pockthg  15610  prmreclem1  15620  4sqlem11  15659  ramub1lem1  15730  ramub1lem2  15731  mreexexlem4d  16307  sscid  16484  latmlej21  17092  latmlej22  17093  lubel  17122  efginvrel1  18141  odadd2  18252  odadd  18253  gexexlem  18255  cyggex2  18298  ablfacrplem  18464  ablfac1c  18470  ablfac1eu  18472  pgpfac1lem3a  18475  isabvd  18820  mptscmfsuppd  18929  znrrg  19914  frlmphl  20120  frlmup1  20137  f1linds  20164  chcoeffeqlem  20690  lmcn2  21452  metrtri  22162  imasdsf1olem  22178  stdbdxmet  22320  nrmmetd  22379  nmmtri  22426  nlmvscnlem2  22489  blcvx  22601  recld2  22617  zdis  22619  opnreen  22634  cnheibor  22754  lebnumlem3  22762  nmoleub2lem3  22915  nmoleub2lem2  22916  nmoleub3  22919  ipcnlem2  23043  cmetcaulem  23086  nglmle  23100  cncmet  23119  csbren  23182  trirn  23183  minveclem4  23203  ovoliunlem1  23270  ovoliun2  23274  ovolscalem1  23281  ovolicopnf  23292  voliunlem2  23319  volsup  23324  ioorcl2  23340  uniiccvol  23348  uniioombllem4  23354  i1fd  23448  mbfi1fseqlem4  23485  itg2const2  23508  itg2eqa  23512  itg2split  23516  itg2i1fseqle  23521  itg2cnlem2  23529  dvcnv  23740  dveflem  23742  dvferm1lem  23747  dvlip2  23758  c1liplem1  23759  dvivthlem1  23771  lhop1lem  23776  dvcvx  23783  dvfsumle  23784  dvfsumabs  23786  dvfsumlem4  23792  dvfsumrlim2  23795  ftc1a  23800  tdeglem4  23820  deg1pwle  23879  fta1blem  23928  aalioulem3  24089  aaliou2b  24096  ulmbdd  24152  ulmdvlem1  24154  itgulm  24162  pserdvlem2  24182  abelthlem3  24187  abelthlem5  24189  abelthlem6  24190  abelthlem7  24192  tanregt0  24285  argimlt0  24359  logdivlti  24366  logcnlem3  24390  logcnlem4  24391  logtayl  24406  logtayl2  24408  cxple2  24443  cxpcn3lem  24488  cxpaddle  24493  isosctrlem1  24548  atantayl  24664  efrlim  24696  dfef2  24697  o1cxp  24701  cxp2lim  24703  divsqrtsumo1  24710  amgmlem  24716  logdifbnd  24720  emcllem7  24728  harmonicbnd4  24737  fsumharmonic  24738  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamucov  24764  lgamcvg2  24781  gamcvg2  24786  ftalem2  24800  basellem2  24808  basellem5  24811  basellem9  24815  vma1  24892  sqff1o  24908  fsumfldivdiaglem  24915  chtub  24937  fsumvma2  24939  chpchtsum  24944  chpub  24945  logfaclbnd  24947  logfacbnd3  24948  logfacrlim  24949  logexprlim  24950  bcmono  25002  bposlem2  25010  bposlem5  25013  bposlem6  25014  lgsne0  25060  lgsquadlem1  25105  lgsquadlem2  25106  2sqblem  25156  chebbnd1lem1  25158  chtppilimlem1  25162  chtppilimlem2  25163  chpchtlim  25168  rplogsumlem1  25173  dchrvmasumiflem1  25190  dchrisum0flblem2  25198  dchrisum0fno1  25200  dchrisum0re  25202  dchrisum0lem2a  25206  dchrisum0lem3  25208  dirith  25218  mulog2sumlem1  25223  mulog2sumlem2  25224  log2sumbnd  25233  selberglem2  25235  logdivbnd  25245  selberg3lem1  25246  selberg4lem1  25249  pntrsumbnd2  25256  pntrlog2bndlem1  25266  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem3  25281  pntlemb  25286  pntlemn  25289  pntlemr  25291  pntlemj  25292  pntlemf  25294  pntlemo  25296  ostth2lem3  25324  ostth3  25327  footeq  25616  hlperpnel  25617  perpdragALT  25619  perpdrag  25620  colperp  25621  mideulem2  25626  opphllem  25627  opphllem3  25641  lmieu  25676  trgcopy  25696  sacgr  25722  acopyeu  25725  usgredgleordALT  26126  eucrctshift  27103  nvabs  27527  smcnlem  27552  ubthlem2  27727  minvecolem4  27736  htthlem  27774  normpyc  28003  nmophmi  28890  hstle  29089  hstles  29090  stlei  29099  nnmulge  29515  fsumiunle  29575  2sqmod  29648  xrge0npcan  29694  archirngz  29743  archiabllem1a  29745  archiabllem2a  29748  archiabllem2c  29749  ornglmulle  29805  orngrmulle  29806  madjusmdetlem2  29894  esumpinfval  30135  esumpinfsum  30139  esumpcvgval  30140  esum2d  30155  esumiun  30156  dya2icoseg  30339  omssubadd  30362  carsgsigalem  30377  carsggect  30380  carsgclctunlem3  30382  omsmeas  30385  eulerpartlems  30422  sgnmulsgn  30611  signsplypnf  30627  signsply0  30628  reprlt  30697  reprinfz1  30700  hgt750lemc  30725  hgt750lemf  30731  resconn  31228  sinccvglem  31566  circum  31568  btwnxfr  32163  nn0prpwlem  32317  dnibndlem2  32469  poimirlem7  33416  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem3  33463  ftc1anc  33493  isbnd3  33583  cntotbnd  33595  bfp  33623  rrndstprj2  33630  1cvrjat  34761  3atlem1  34769  3atlem6  34774  llnmlplnN  34825  2llnjaN  34852  2lplnja  34905  dalem57  35015  dalawlem11  35167  dalawlem12  35168  lhp2lt  35287  lhpj1  35308  lhpm0atN  35315  4atexlemex2  35357  lautm  35380  cdleme17b  35574  cdleme20j  35606  cdleme30a  35666  cdlemg4c  35900  cdlemg17a  35949  cdlemg31c  35987  trljco  36028  cdlemk46  36236  dia2dimlem2  36354  cdlemm10N  36407  cdlemn10  36495  dihmeetlem1N  36579  dihglblem5apreN  36580  dihmeetlem15N  36610  mapdat  36956  irrapxlem1  37386  irrapxlem4  37389  pell1qrgaplem  37437  pellfundglb  37449  rmspecfund  37474  monotoddzzfi  37507  rmynn  37523  jm2.24nn  37526  jm2.17c  37529  jm2.24  37530  acongeq  37550  jm2.20nn  37564  jm2.26lem3  37568  jm2.27a  37572  jm2.27c  37574  rmydioph  37581  jm3.1lem2  37585  frlmpwfi  37668  areaquad  37802  rp-isfinite6  37864  frege129d  38055  leeq1d  38455  imo72b2  38475  cvgdvgrat  38512  radcnvrat  38513  hashnzfzclim  38521  isosctrlem1ALT  39170  cncmpmax  39191  iooabslt  39721  fmul01lt1lem2  39817  clim1fr1  39833  limcrecl  39861  climxrrelem  39981  stoweidlem1  40218  stoweidlem11  40228  stoweidlem14  40231  stoweidlem24  40241  stoweidlem26  40243  wallispilem4  40285  wallispilem5  40286  stirlinglem1  40291  fourierdlem51  40374  fourierdlem65  40388  fouriersw  40448  2leaddle2  41312  sqrtpwpw2p  41450  lighneallem4a  41525  flnn0div2ge  42327  logbpw2m1  42361  amgmwlem  42548