Theorem eqbrtrrd 5116

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  dftpos4  8178  dif1en  9075  fodomfi  9201  fodomfiOLD  9220  fmptssfisupp  9284  resfifsupp  9287  cnfcom2lem  9597  dmttrcl  9617  ttrclselem2  9622  ficardadju  10094  enfin1ai  10278  pwcfsdom  10477  fpwwe2lem6  10530  fpwwe2  10537  canthp1lem1  10546  1nqenq  10856  prlem936  10941  lemulge11  11987  supaddc  12092  supmul1  12094  mul2lt0llt0  12999  mul2lt0lgt0  13000  xaddge0  13160  xadddi2  13199  ltexp2a  14073  leexp2a  14079  nnlesq  14112  digit1  14144  faclbnd4lem1  14200  faclbnd6  14206  facavg  14208  prsshashgt1  14317  nehash2  14381  abs3dif  15239  abs2dif  15240  limsupgre  15388  rlimclim1  15452  rlimuni  15457  rlimres2  15468  rlimcn1  15495  rlimcn1b  15496  recn2  15508  imcn2  15509  rlimo1  15524  o1rlimmul  15526  iserex  15564  isercoll  15575  caucvgrlem2  15582  caucvgr  15583  iseraltlem3  15591  summolem2a  15622  fsumge1  15704  o1fsum  15720  isumrpcl  15750  climcnds  15758  harmonic  15766  mertenslem1  15791  prodmolem2a  15841  ege2le3  15997  efgt1p2  16023  efgt1p  16024  eirrlem  16113  rpnnen2lem11  16133  fsumdvds  16219  bitsfzo  16346  bitsmod  16347  bitscmp  16349  mulgcd  16459  dvdssqlem  16477  nn0seqcvgd  16481  mulgcddvds  16566  rpdvds  16571  qden1elz  16668  phimullem  16690  hashgcdlem  16699  hashgcdeq  16701  pcdvdstr  16788  pockthg  16818  prmreclem1  16828  4sqlem11  16867  ramub1lem1  16938  ramub1lem2  16939  mreexexlem4d  17553  sscid  17731  latmlej21  18386  latmlej22  18387  lubel  18420  efginvrel1  19607  odadd2  19728  odadd  19729  gexexlem  19731  cyggex2  19776  ablfacrplem  19946  ablfac1c  19952  ablfac1eu  19954  pgpfac1lem3a  19957  isabvd  20697  ornglmulle  20752  orngrmulle  20753  mptscmfsuppd  20831  znrrg  21472  frlmphl  21688  frlmup1  21705  f1linds  21732  psdmplcl  22047  chcoeffeqlem  22770  lmcn2  23534  metrtri  24243  imasdsf1olem  24259  stdbdxmet  24401  nrmmetd  24460  nmmtri  24508  nlmvscnlem2  24571  blcvx  24684  recld2  24701  zdis  24703  opnreen  24718  cnheibor  24852  lebnumlem3  24860  nmoleub2lem3  25013  nmoleub2lem2  25014  nmoleub3  25017  ipcnlem2  25142  cmetcaulem  25186  nglmle  25200  cncmet  25220  csbren  25297  trirn  25298  minveclem4  25330  ovoliunlem1  25401  ovoliun2  25405  ovolscalem1  25412  ovolicopnf  25423  voliunlem2  25450  volsup  25455  ioorcl2  25471  uniiccvol  25479  uniioombllem4  25485  i1fd  25580  mbfi1fseqlem4  25617  itg2const2  25640  itg2eqa  25644  itg2split  25648  itg2i1fseqle  25653  itg2cnlem2  25661  dvcnv  25879  dveflem  25881  dvferm1lem  25886  dvlip2  25898  c1liplem1  25899  dvivthlem1  25911  lhop1lem  25916  dvcvx  25923  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  dvfsumlem4  25934  dvfsumrlim2  25937  ftc1a  25942  tdeglem4  25963  deg1pwle  26023  fta1blem  26074  aalioulem3  26240  aaliou2b  26247  ulmbdd  26305  ulmdvlem1  26307  itgulm  26315  pserdvlem2  26336  abelthlem3  26341  abelthlem5  26343  abelthlem6  26344  abelthlem7  26346  tanregt0  26446  argimlt0  26520  logdivlti  26527  logcnlem3  26551  logcnlem4  26552  logtayl  26567  logtayl2  26569  cxple2  26604  cxpcn3lem  26655  cxpaddle  26660  rtprmirr  26668  isosctrlem1  26726  atantayl  26845  efrlim  26877  efrlimOLD  26878  dfef2  26879  o1cxp  26883  cxp2lim  26885  divsqrtsumo1  26892  amgmlem  26898  logdifbnd  26902  emcllem7  26910  harmonicbnd4  26919  fsumharmonic  26920  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamucov  26946  lgamcvg2  26963  gamcvg2  26968  ftalem2  26982  basellem2  26990  basellem5  26993  basellem9  26997  vma1  27074  sqff1o  27090  fsumfldivdiaglem  27097  chtub  27121  fsumvma2  27123  chpchtsum  27128  chpub  27129  logfaclbnd  27131  logfacbnd3  27132  logfacrlim  27133  logexprlim  27134  bcmono  27186  bposlem2  27194  bposlem5  27197  bposlem6  27198  lgsne0  27244  lgsquadlem1  27289  lgsquadlem2  27290  2sqblem  27340  2sqmod  27345  chebbnd1lem1  27378  chtppilimlem1  27382  chtppilimlem2  27383  chpchtlim  27388  rplogsumlem1  27393  dchrvmasumiflem1  27410  dchrisum0flblem2  27418  dchrisum0fno1  27420  dchrisum0lem2a  27426  dchrisum0lem3  27428  dirith  27438  mulog2sumlem1  27443  mulog2sumlem2  27444  log2sumbnd  27453  selberglem2  27455  logdivbnd  27465  selberg3lem1  27466  selberg4lem1  27469  pntrsumbnd2  27476  pntrlog2bndlem1  27486  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntpbnd1a  27494  pntpbnd1  27495  pntpbnd2  27496  pntibndlem3  27501  pntlemb  27506  pntlemn  27509  pntlemr  27511  pntlemj  27512  pntlemf  27514  pntlemo  27516  ostth2lem3  27544  ostth3  27547  addsuniflem  27913  sltp1d  27927  negsid  27952  negsunif  27966  mulsuniflem  28057  precsexlem9  28122  n0sge0  28235  zscut  28300  halfcut  28346  addhalfcut  28347  footeq  28669  hlperpnel  28670  perpdragALT  28672  perpdrag  28673  colperp  28674  mideulem2  28679  opphllem  28680  opphllem3  28694  lmieu  28729  trgcopy  28749  sacgr  28776  acopyeu  28779  usgredgleordALT  29179  eucrctshift  30187  nvabs  30616  smcnlem  30641  ubthlem2  30815  minvecolem4  30824  htthlem  30861  normpyc  31090  nmophmi  31975  hstle  32174  hstles  32175  stlei  32184  f1rnen  32571  nnmulge  32682  fsumiunle  32774  sgnmulsgn  32787  wrdt2ind  32895  xrge0npcan  32974  gsumwrd2dccat  33020  trsp2cyc  33065  archirngz  33131  archiabllem1a  33133  archiabllem2a  33136  archiabllem2c  33137  elrgspnlem1  33182  elrgspn  33186  elrgspnsubrunlem2  33188  rprmasso  33462  q1pdir  33535  r1pquslmic  33543  mplvrpmga  33546  drngdimgt0  33585  lbsdiflsp0  33593  fldextrspundgle  33645  fldext2rspun  33649  minplyirredlem  33677  madjusmdetlem2  33795  esumpinfval  34040  esumpinfsum  34044  esumpcvgval  34045  esum2d  34060  esumiun  34061  dya2icoseg  34245  omssubadd  34268  carsgsigalem  34283  carsggect  34286  carsgclctunlem3  34288  omsmeas  34291  eulerpartlems  34328  signsplypnf  34518  signsply0  34519  reprlt  34587  reprinfz1  34590  hgt750lemc  34615  hgt750lemf  34621  pthhashvtx  35105  resconn  35223  sinccvglem  35649  circum  35651  btwnxfr  36034  nn0prpwlem  36300  dnibndlem2  36457  unblimceq0  36485  irrdiff  37304  poimirlem7  37611  mblfinlem3  37643  mblfinlem4  37644  itg2addnclem3  37657  ftc1anc  37685  isbnd3  37768  cntotbnd  37780  bfp  37808  rrndstprj2  37815  1cvrjat  39458  3atlem1  39466  3atlem6  39471  llnmlplnN  39522  2llnjaN  39549  2lplnja  39602  dalem57  39712  dalawlem11  39864  dalawlem12  39865  lhp2lt  39984  lhpj1  40005  lhpm0atN  40012  4atexlemex2  40054  lautm  40077  cdleme17b  40270  cdleme20j  40301  cdleme30a  40361  cdlemg4c  40595  cdlemg17a  40644  cdlemg31c  40682  trljco  40723  cdlemk46  40931  dia2dimlem2  41048  cdlemm10N  41101  cdlemn10  41189  dihmeetlem1N  41273  dihglblem5apreN  41274  dihmeetlem15N  41304  mapdat  41650  lcmineqlem19  42024  lcmineqlem20  42025  aks4d1p1p5  42052  aks4d1p8d2  42062  aks4d1p8  42064  aks4d1p9  42065  hashscontpow  42099  dvdsexpnn  42310  mullt0b1d  42460  selvvvval  42562  evlselv  42564  mhphflem  42573  fltnlta  42640  3cubeslem1  42661  irrapxlem1  42799  irrapxlem4  42802  pell1qrgaplem  42850  pellfundglb  42862  rmspecfund  42886  monotoddzzfi  42919  rmynn  42933  jm2.24nn  42936  jm2.17c  42939  jm2.24  42940  acongeq  42960  jm2.20nn  42974  jm2.26lem3  42978  jm2.27a  42982  jm2.27c  42984  rmydioph  42991  jm3.1lem2  42995  frlmpwfi  43075  areaquad  43193  cantnf2  43302  rp-isfinite6  43495  frege129d  43740  leeq1d  44134  imo72b2lem0  44142  imo72b2  44149  cvgdvgrat  44290  radcnvrat  44291  hashnzfzclim  44299  isosctrlem1ALT  44911  cncmpmax  45014  iooabslt  45484  fmul01lt1lem2  45570  clim1fr1  45586  limcrecl  45614  climxrrelem  45734  liminflbuz2  45800  dvnprodlem1  45931  stoweidlem1  45986  stoweidlem11  45996  stoweidlem14  45999  stoweidlem24  46009  stoweidlem26  46011  wallispilem4  46053  wallispilem5  46054  stirlinglem1  46059  fourierdlem51  46142  fourierdlem65  46156  fouriersw  46216  2leaddle2  47286  sqrtpwpw2p  47526  lighneallem4a  47596  flnn0div2ge  48522  logbpw2m1  48556  functermclem  49496  amgmwlem  49791