Theorem eqbrtrrd 5129

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  dftpos4  8262  dif1en  9177  fodomfi  9304  fmptssfisupp  9386  cnfcom2lem  9702  dmttrcl  9722  ttrclselem2  9727  ficardadju  10278  enfin1ai  10462  pwcfsdom  10668  fpwwe2lem6  10721  fpwwe2  10728  canthp1lem1  10737  1nqenq  11047  prlem936  11132  lemulge11  12179  supaddc  12284  supmul1  12286  mul2lt0llt0  13226  mul2lt0lgt0  13227  xaddge0  13388  xadddi2  13427  ltexp2a  14309  leexp2a  14315  nnlesq  14349  digit1  14381  faclbnd4lem1  14437  faclbnd6  14443  facavg  14445  prsshashgt1  14555  nehash2  14619  sgnmulsgn  15262  abs3dif  15499  abs2dif  15500  limsupgre  15648  rlimclim1  15712  rlimuni  15717  rlimres2  15728  rlimcn1  15755  rlimcn1b  15756  recn2  15768  imcn2  15769  rlimo1  15784  o1rlimmul  15786  iserex  15824  isercoll  15835  caucvgrlem2  15842  caucvgr  15843  iseraltlem3  15851  summolem2a  15881  fsumge1  15964  o1fsum  15980  isumrpcl  16012  climcnds  16020  harmonic  16028  mertenslem1  16053  prodmolem2a  16101  ege2le3  16256  efgt1p2  16282  efgt1p  16283  eirrlem  16372  rpnnen2lem11  16392  fsumdvds  16478  bitsfzo  16605  bitsmod  16606  bitscmp  16608  mulgcd  16721  dvdsexpnn  16740  nn0seqcvgd  16745  mulgcddvds  16830  rpdvds  16835  qden1elz  16933  phimullem  16956  hashgcdlem  16965  hashgcdeq  16967  pcdvdstr  17054  pockthg  17084  prmreclem1  17094  4sqlem11  17133  ramub1lem1  17204  ramub1lem2  17205  mreexexlem4d  17821  sscid  17999  latmlej21  18654  latmlej22  18655  lubel  18688  efginvrel1  19942  odadd2  20063  odadd  20064  gexexlem  20066  cyggex2  20111  ablfacrplem  20281  ablfac1c  20287  ablfac1eu  20289  pgpfac1lem3a  20292  isabvd  21069  ornglmulle  21124  orngrmulle  21125  mptscmfsuppd  21203  znrrg  21871  frlmphl  22087  frlmup1  22104  f1linds  22131  selvvvval  22451  psdmplcl  22483  chcoeffeqlem  23203  lmcn2  23968  metrtri  24676  imasdsf1olem  24692  stdbdxmet  24834  nrmmetd  24893  nmmtri  24941  nlmvscnlem2  25004  blcvx  25117  recld2  25134  zdis  25136  opnreen  25151  cnheibor  25276  lebnumlem3  25284  nmoleub2lem3  25436  nmoleub2lem2  25437  nmoleub3  25440  ipcnlem2  25565  cmetcaulem  25609  nglmle  25623  cncmet  25643  csbren  25720  trirn  25721  minveclem4  25753  ovoliunlem1  25823  ovoliun2  25827  ovolscalem1  25834  ovolicopnf  25845  voliunlem2  25872  volsup  25877  ioorcl2  25893  uniiccvol  25901  uniioombllem4  25907  i1fd  26002  mbfi1fseqlem4  26039  itg2const2  26062  itg2eqa  26066  itg2split  26070  itg2i1fseqle  26075  itg2cnlem2  26083  dvcnv  26297  dveflem  26299  dvferm1lem  26304  dvlip2  26315  c1liplem1  26316  dvivthlem1  26328  lhop1lem  26333  dvcvx  26340  dvfsumle  26341  dvfsumabs  26343  dvfsumlem4  26349  dvfsumrlim2  26352  ftc1a  26357  tdeglem4  26378  deg1pwle  26438  fta1blem  26489  aalioulem3  26661  aaliou2b  26668  ulmbdd  26725  ulmdvlem1  26727  itgulm  26735  pserdvlem2  26755  abelthlem3  26760  abelthlem5  26762  abelthlem6  26763  abelthlem7  26765  tanregt0  26867  argimlt0  26941  logdivlti  26948  logcnlem3  26972  logcnlem4  26973  logtayl  26988  logtayl2  26990  cxple2  27025  cxpcn3lem  27075  cxpaddle  27080  rtprmirr  27088  isosctrlem1  27146  atantayl  27265  efrlim  27297  dfef2  27298  o1cxp  27302  cxp2lim  27304  divsqrtsumo1  27311  amgmlem  27317  logdifbnd  27321  emcllem7  27329  harmonicbnd4  27338  fsumharmonic  27339  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamucov  27365  lgamcvg2  27382  gamcvg2  27387  ftalem2  27401  basellem2  27409  basellem5  27412  basellem9  27416  vma1  27493  sqff1o  27509  fsumfldivdiaglem  27516  chtub  27539  fsumvma2  27541  chpchtsum  27546  chpub  27547  logfaclbnd  27549  logfacbnd3  27550  logfacrlim  27551  logexprlim  27552  bcmono  27604  bposlem2  27612  bposlem5  27615  bposlem6  27616  lgsne0  27662  lgsquadlem1  27707  lgsquadlem2  27708  2sqblem  27758  2sqmod  27763  chebbnd1lem1  27796  chtppilimlem1  27800  chtppilimlem2  27801  chpchtlim  27806  rplogsumlem1  27811  dchrvmasumiflem1  27828  dchrisum0flblem2  27836  dchrisum0fno1  27838  dchrisum0lem2a  27844  dchrisum0lem3  27846  dirith  27856  mulog2sumlem1  27861  mulog2sumlem2  27862  log2sumbnd  27871  selberglem2  27873  logdivbnd  27883  selberg3lem1  27884  selberg4lem1  27887  pntrsumbnd2  27894  pntrlog2bndlem1  27904  pntrlog2bndlem5  27908  pntrlog2bndlem6  27910  pntpbnd1a  27912  pntpbnd1  27913  pntpbnd2  27914  pntibndlem3  27919  pntlemb  27924  pntlemn  27927  pntlemr  27929  pntlemj  27930  pntlemf  27932  pntlemo  27934  ostth2lem3  27962  ostth3  27965  addsuniflem  28387  ltsp1d  28401  negsid  28427  negsunif  28441  negleft  28444  mulsuniflem  28535  precsexlem9  28601  n0sge0  28724  zcuts  28793  halfcut  28844  addhalfcut  28845  pw2cut2  28848  bdayfinbndlem1  28853  footeq  29199  hlperpnel  29201  perpdragALT  29203  perpdrag  29204  colperp  29205  mideulem2  29210  opphllem  29211  opphllem3  29225  lmieu  29289  trgcopy  29311  sacgr  29339  acopyeu  29342  perpeqlem  29347  angmgmaddcpbl  29390  perpprlng  29428  prlngmid2  29439  usgredgleordALT  29815  pthhashvtx  30315  eucrctshift  30844  nvabs  31274  smcnlem  31299  ubthlem2  31473  minvecolem4  31482  htthlem  31519  normpyc  31748  nmophmi  32633  hstle  32832  hstles  32833  stlei  32842  f1rnen  33222  nnmulge  33331  fsumiunle  33420  wrdt2ind  33516  xrge0npcan  33581  gsumwrd2dccat  33639  trsp2cyc  33684  archirngz  33750  archiabllem1a  33752  archiabllem2a  33755  archiabllem2c  33756  elrgspnlem1  33803  elrgspn  33807  elrgspnsubrunlem2  33809  rprmasso  34057  q1pdir  34135  r1pquslmic  34142  selvply1rhmlema  34150  selvply1rhmlem1  34152  evlextv  34174  mplvrpmga  34177  mplvrpmrhm  34179  drngdimgt0  34250  lbsdiflsp0  34258  fldextrspundgle  34310  fldext2rspun  34314  minplyirredlem  34342  madjusmdetlem2  34460  esumpinfval  34705  esumpinfsum  34709  esumpcvgval  34710  esum2d  34725  esumiun  34726  dya2icoseg  34909  omssubadd  34932  carsgsigalem  34947  carsggect  34950  carsgclctunlem3  34952  omsmeas  34955  eulerpartlems  34992  signsplypnf  35179  signsply0  35180  reprlt  35248  reprinfz1  35251  hgt750lemc  35276  hgt750lemf  35282  resconn  36011  sinccvglem  36437  circum  36439  btwnxfr  36821  nn0prpwlem  37110  dnibndlem2  37345  unblimceq0  37373  irrdiff  38247  poimirlem7  38545  mblfinlem3  38577  mblfinlem4  38578  itg2addnclem3  38591  ftc1anc  38619  isbnd3  38718  cntotbnd  38730  bfp  38758  rrndstprj2  38765  1cvrjat  40532  3atlem1  40540  3atlem6  40545  llnmlplnN  40596  2llnjaN  40623  2lplnja  40676  dalem57  40786  dalawlem11  40938  dalawlem12  40939  lhp2lt  41058  lhpj1  41079  lhpm0atN  41086  4atexlemex2  41128  lautm  41151  cdleme17b  41344  cdleme20j  41375  cdleme30a  41435  cdlemg4c  41669  cdlemg17a  41718  cdlemg31c  41756  trljco  41797  cdlemk46  42005  dia2dimlem2  42122  cdlemm10N  42175  cdlemn10  42263  dihmeetlem1N  42347  dihglblem5apreN  42348  dihmeetlem15N  42378  mapdat  42724  lcmineqlem19  43097  lcmineqlem20  43098  aks4d1p1p5  43125  aks4d1p8d2  43135  aks4d1p8  43137  aks4d1p9  43138  hashscontpow  43172  mullt0b1d  43547  evlselv  43617  mhphflem  43624  fltnlta  43674  3cubeslem1  43694  irrapxlem1  43828  irrapxlem4  43831  pell1qrgaplem  43879  pellfundglb  43891  rmspecfund  43915  monotoddzzfi  43948  rmynn  43962  jm2.24nn  43965  jm2.17c  43968  jm2.24  43969  acongeq  43989  jm2.20nn  44003  jm2.26lem3  44007  jm2.27a  44011  jm2.27c  44013  rmydioph  44020  jm3.1lem2  44024  frlmpwfi  44099  areaquad  44217  cantnf2  44326  rp-isfinite6  44518  frege129d  44762  leeq1d  45156  imo72b2lem0  45164  imo72b2  45171  cvgdvgrat  45296  radcnvrat  45297  hashnzfzclim  45305  isosctrlem1ALT  45915  cncmpmax  46048  iooabslt  46510  fmul01lt1lem2  46596  clim1fr1  46612  limcrecl  46640  climxrrelem  46758  liminflbuz2  46824  dvnprodlem1  46955  stoweidlem1  47010  stoweidlem11  47020  stoweidlem14  47023  stoweidlem24  47033  stoweidlem26  47035  wallispilem4  47077  wallispilem5  47078  stirlinglem1  47083  fourierdlem51  47166  fourierdlem65  47180  fouriersw  47240  2leaddle2  48367  2timesltsqm1  48448  sqrtpwpw2p  48622  lighneallem4a  48692  flnn0div2ge  49644  logbpw2m1  49678  functermclem  50614  amgmwlem  50986