Theorem eqbrtrrd 5135

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109

This theorem is used by:  dftpos4  8300  dif1en  9215  fodomfi  9342  fmptssfisupp  9423  cnfcom2lem  9739  dmttrcl  9759  ttrclselem2  9764  ficardadju  10317  enfin1ai  10501  pwcfsdom  10707  fpwwe2lem6  10760  fpwwe2  10767  canthp1lem1  10776  1nqenq  11086  prlem936  11171  lemulge11  12219  supaddc  12324  supmul1  12326  mul2lt0llt0  13266  mul2lt0lgt0  13267  xaddge0  13428  xadddi2  13467  ltexp2a  14349  leexp2a  14355  nnlesq  14389  digit1  14422  faclbnd4lem1  14478  faclbnd6  14484  facavg  14486  prsshashgt1  14596  nehash2  14660  sgnmulsgn  15305  abs3dif  15542  abs2dif  15543  limsupgre  15692  rlimclim1  15756  rlimuni  15761  rlimres2  15772  rlimcn1  15799  rlimcn1b  15800  recn2  15812  imcn2  15813  rlimo1  15828  o1rlimmul  15830  iserex  15868  isercoll  15879  caucvgrlem2  15886  caucvgr  15887  iseraltlem3  15895  summolem2a  15925  fsumge1  16008  o1fsum  16024  isumrpcl  16056  climcnds  16064  harmonic  16072  mertenslem1  16097  prodmolem2a  16145  ege2le3  16300  efgt1p2  16326  efgt1p  16327  eirrlem  16416  rpnnen2lem11  16436  fsumdvds  16522  bitsfzo  16649  bitsmod  16650  bitscmp  16652  mulgcd  16765  dvdsexpnn  16784  nn0seqcvgd  16789  mulgcddvds  16874  rpdvds  16879  qden1elz  16977  phimullem  17000  hashgcdlem  17009  hashgcdeq  17011  pcdvdstr  17098  pockthg  17128  prmreclem1  17138  4sqlem11  17177  ramub1lem1  17248  ramub1lem2  17249  mreexexlem4d  17871  sscid  18049  latmlej21  18704  latmlej22  18705  lubel  18738  efginvrel1  19993  odadd2  20114  odadd  20115  gexexlem  20117  cyggex2  20162  ablfacrplem  20332  ablfac1c  20338  ablfac1eu  20340  pgpfac1lem3a  20343  isabvd  21120  ornglmulle  21175  orngrmulle  21176  mptscmfsuppd  21254  znrrg  21926  frlmphl  22142  frlmup1  22159  f1linds  22186  selvvvval  22506  psdmplcl  22538  chcoeffeqlem  23258  lmcn2  24023  metrtri  24731  imasdsf1olem  24747  stdbdxmet  24889  nrmmetd  24948  nmmtri  24996  nlmvscnlem2  25059  blcvx  25172  recld2  25189  zdis  25191  opnreen  25206  cnheibor  25331  lebnumlem3  25339  nmoleub2lem3  25491  nmoleub2lem2  25492  nmoleub3  25495  ipcnlem2  25620  cmetcaulem  25664  nglmle  25678  cncmet  25698  csbren  25775  trirn  25776  minveclem4  25808  ovoliunlem1  25878  ovoliun2  25882  ovolscalem1  25889  ovolicopnf  25900  voliunlem2  25927  volsup  25932  ioorcl2  25948  uniiccvol  25956  uniioombllem4  25962  i1fd  26057  mbfi1fseqlem4  26094  itg2const2  26117  itg2eqa  26121  itg2split  26125  itg2i1fseqle  26130  itg2cnlem2  26138  dvcnv  26352  dveflem  26354  dvferm1lem  26359  dvlip2  26370  c1liplem1  26371  dvivthlem1  26383  lhop1lem  26388  dvcvx  26395  dvfsumle  26396  dvfsumabs  26398  dvfsumlem4  26404  dvfsumrlim2  26407  ftc1a  26412  tdeglem4  26433  deg1pwle  26493  fta1blem  26544  aalioulem3  26718  aaliou2b  26725  ulmbdd  26782  ulmdvlem1  26784  itgulm  26792  pserdvlem2  26812  abelthlem3  26817  abelthlem5  26819  abelthlem6  26820  abelthlem7  26822  tanregt0  26924  argimlt0  26998  logdivlti  27005  logcnlem3  27029  logcnlem4  27030  logtayl  27045  logtayl2  27047  cxple2  27082  cxpcn3lem  27132  cxpaddle  27137  rtprmirr  27145  isosctrlem1  27203  atantayl  27322  efrlim  27354  dfef2  27355  o1cxp  27359  cxp2lim  27361  divsqrtsumo1  27368  amgmlem  27374  logdifbnd  27378  emcllem7  27386  harmonicbnd4  27395  fsumharmonic  27396  lgamgulmlem2  27414  lgamgulmlem3  27415  lgamucov  27422  lgamcvg2  27439  gamcvg2  27444  ftalem2  27458  basellem2  27466  basellem5  27469  basellem9  27473  vma1  27550  sqff1o  27566  fsumfldivdiaglem  27573  chtub  27596  fsumvma2  27598  chpchtsum  27603  chpub  27604  logfaclbnd  27606  logfacbnd3  27607  logfacrlim  27608  logexprlim  27609  bcmono  27661  bposlem2  27669  bposlem5  27672  bposlem6  27673  lgsne0  27719  lgsquadlem1  27764  lgsquadlem2  27765  2sqblem  27815  2sqmod  27820  chebbnd1lem1  27853  chtppilimlem1  27857  chtppilimlem2  27858  chpchtlim  27863  rplogsumlem1  27868  dchrvmasumiflem1  27885  dchrisum0flblem2  27893  dchrisum0fno1  27895  dchrisum0lem2a  27901  dchrisum0lem3  27903  dirith  27913  mulog2sumlem1  27918  mulog2sumlem2  27919  log2sumbnd  27928  selberglem2  27930  logdivbnd  27940  selberg3lem1  27941  selberg4lem1  27944  pntrsumbnd2  27951  pntrlog2bndlem1  27961  pntrlog2bndlem5  27965  pntrlog2bndlem6  27967  pntpbnd1a  27969  pntpbnd1  27970  pntpbnd2  27971  pntibndlem3  27976  pntlemb  27981  pntlemn  27984  pntlemr  27986  pntlemj  27987  pntlemf  27989  pntlemo  27991  ostth2lem3  28019  ostth3  28022  addsuniflem  28444  ltsp1d  28458  negsid  28484  negsunif  28498  negleft  28501  mulsuniflem  28592  precsexlem9  28658  n0sge0  28781  zcuts  28850  halfcut  28901  addhalfcut  28902  pw2cut2  28905  bdayfinbndlem1  28910  footeq  29256  hlperpnel  29258  perpdragALT  29260  perpdrag  29261  colperp  29262  mideulem2  29267  opphllem  29268  opphllem3  29282  lmieu  29346  trgcopy  29368  sacgr  29396  acopyeu  29399  perpeqlem  29404  angmgmaddcpbl  29447  perpprlng  29485  prlngmid2  29496  usgredgleordALT  29872  pthhashvtx  30372  eucrctshift  30901  nvabs  31331  smcnlem  31356  ubthlem2  31530  minvecolem4  31539  htthlem  31576  normpyc  31805  nmophmi  32690  hstle  32889  hstles  32890  stlei  32899  f1rnen  33320  nnmulge  33427  fsumiunle  33516  wrdt2ind  33612  xrge0npcan  33680  gsumwrd2dccat  33738  trsp2cyc  33783  archirngz  33849  archiabllem1a  33851  archiabllem2a  33854  archiabllem2c  33855  elrgspnlem1  33902  elrgspn  33906  elrgspnsubrunlem2  33908  rprmasso  34161  q1pdir  34240  r1pquslmic  34247  rngunsnply1chr2lem1  34250  selvply1rhmlema  34261  selvply1rhmlem1  34263  evlextv  34285  mplvrpmga  34288  mplvrpmrhm  34290  drngdimgt0  34361  lbsdiflsp0  34369  fldextrspundgle  34421  fldext2rspun  34425  minplyirredlem  34453  madjusmdetlem2  34571  esumpinfval  34816  esumpinfsum  34820  esumpcvgval  34821  esum2d  34836  esumiun  34837  dya2icoseg  35020  omssubadd  35043  carsgsigalem  35058  carsggect  35061  carsgclctunlem3  35063  omsmeas  35066  eulerpartlems  35103  signsplypnf  35290  signsply0  35291  reprlt  35359  reprinfz1  35362  hgt750lemc  35387  hgt750lemf  35393  resconn  36219  sinccvglem  36645  circum  36647  btwnxfr  37036  nn0prpwlem  37325  dnibndlem2  37560  unblimceq0  37588  irrdiff  38515  poimirlem7  38813  mblfinlem3  38845  mblfinlem4  38846  itg2addnclem3  38859  ftc1anc  38887  isbnd3  38984  cntotbnd  38996  bfp  39024  rrndstprj2  39031  1cvrjat  40798  3atlem1  40806  3atlem6  40811  llnmlplnN  40862  2llnjaN  40889  2lplnja  40942  dalem57  41052  dalawlem11  41204  dalawlem12  41205  lhp2lt  41324  lhpj1  41345  lhpm0atN  41352  4atexlemex2  41394  lautm  41417  cdleme17b  41610  cdleme20j  41641  cdleme30a  41701  cdlemg4c  41935  cdlemg17a  41984  cdlemg31c  42022  trljco  42063  cdlemk46  42271  dia2dimlem2  42388  cdlemm10N  42441  cdlemn10  42529  dihmeetlem1N  42613  dihglblem5apreN  42614  dihmeetlem15N  42644  mapdat  42990  lcmineqlem19  43363  lcmineqlem20  43364  aks4d1p1p5  43391  aks4d1p8d2  43401  aks4d1p8  43403  aks4d1p9  43404  hashscontpow  43438  mullt0b1d  43813  evlselv  43883  mhphflem  43890  fltnlta  43940  3cubeslem1  43960  irrapxlem1  44095  irrapxlem4  44098  pell1qrgaplem  44146  pellfundglb  44158  rmspecfund  44182  monotoddzzfi  44215  rmynn  44229  jm2.24nn  44232  jm2.17c  44235  jm2.24  44236  acongeq  44256  jm2.20nn  44270  jm2.26lem3  44274  jm2.27a  44278  jm2.27c  44280  rmydioph  44287  jm3.1lem2  44291  frlmpwfi  44366  areaquad  44479  cantnf2  44588  rp-isfinite6  44780  frege129d  45024  leeq1d  45418  imo72b2lem0  45426  imo72b2  45433  cvgdvgrat  45558  radcnvrat  45559  hashnzfzclim  45567  isosctrlem1ALT  46176  cncmpmax  46323  iooabslt  46784  fmul01lt1lem2  46870  clim1fr1  46886  limcrecl  46914  climxrrelem  47032  liminflbuz2  47098  dvnprodlem1  47229  stoweidlem1  47284  stoweidlem11  47294  stoweidlem14  47297  stoweidlem24  47307  stoweidlem26  47309  wallispilem4  47351  wallispilem5  47352  stirlinglem1  47357  fourierdlem51  47440  fourierdlem65  47454  fouriersw  47514  2leaddle2  48641  2timesltsqm1  48722  sqrtpwpw2p  48896  lighneallem4a  48966  flnn0div2ge  49976  logbpw2m1  50010  functermclem  50973  amgmwlem  51415