Theorem eqbrtrrd 5172

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149

This theorem is referenced by:  dftpos4  8269  dif1en  9199  dif1enOLD  9201  fodomfi  9348  fodomfiOLD  9368  fmptssfisupp  9432  resfifsupp  9435  cnfcom2lem  9739  dmttrcl  9759  ttrclselem2  9764  ficardadju  10238  enfin1ai  10422  pwcfsdom  10621  fpwwe2lem6  10674  fpwwe2  10681  canthp1lem1  10690  1nqenq  11000  prlem936  11085  lemulge11  12128  supaddc  12233  supmul1  12235  mul2lt0llt0  13137  mul2lt0lgt0  13138  xaddge0  13297  xadddi2  13336  ltexp2a  14203  leexp2a  14209  nnlesq  14241  digit1  14273  faclbnd4lem1  14329  faclbnd6  14335  facavg  14337  prsshashgt1  14446  nehash2  14510  abs3dif  15367  abs2dif  15368  limsupgre  15514  rlimclim1  15578  rlimuni  15583  rlimres2  15594  rlimcn1  15621  rlimcn1b  15622  recn2  15634  imcn2  15635  rlimo1  15650  o1rlimmul  15652  iserex  15690  isercoll  15701  caucvgrlem2  15708  caucvgr  15709  iseraltlem3  15717  summolem2a  15748  fsumge1  15830  o1fsum  15846  isumrpcl  15876  climcnds  15884  harmonic  15892  mertenslem1  15917  prodmolem2a  15967  ege2le3  16123  efgt1p2  16147  efgt1p  16148  eirrlem  16237  rpnnen2lem11  16257  fsumdvds  16342  bitsfzo  16469  bitsmod  16470  bitscmp  16472  mulgcd  16582  dvdssqlem  16600  nn0seqcvgd  16604  mulgcddvds  16689  rpdvds  16694  qden1elz  16791  phimullem  16813  hashgcdlem  16822  hashgcdeq  16823  pcdvdstr  16910  pockthg  16940  prmreclem1  16950  4sqlem11  16989  ramub1lem1  17060  ramub1lem2  17061  mreexexlem4d  17692  sscid  17872  latmlej21  18538  latmlej22  18539  lubel  18572  efginvrel1  19761  odadd2  19882  odadd  19883  gexexlem  19885  cyggex2  19930  ablfacrplem  20100  ablfac1c  20106  ablfac1eu  20108  pgpfac1lem3a  20111  isabvd  20830  mptscmfsuppd  20943  znrrg  21602  frlmphl  21819  frlmup1  21836  f1linds  21863  psdmplcl  22184  chcoeffeqlem  22907  lmcn2  23673  metrtri  24383  imasdsf1olem  24399  stdbdxmet  24544  nrmmetd  24603  nmmtri  24651  nlmvscnlem2  24722  blcvx  24834  recld2  24850  zdis  24852  opnreen  24867  cnheibor  25001  lebnumlem3  25009  nmoleub2lem3  25162  nmoleub2lem2  25163  nmoleub3  25166  ipcnlem2  25292  cmetcaulem  25336  nglmle  25350  cncmet  25370  csbren  25447  trirn  25448  minveclem4  25480  ovoliunlem1  25551  ovoliun2  25555  ovolscalem1  25562  ovolicopnf  25573  voliunlem2  25600  volsup  25605  ioorcl2  25621  uniiccvol  25629  uniioombllem4  25635  i1fd  25730  mbfi1fseqlem4  25768  itg2const2  25791  itg2eqa  25795  itg2split  25799  itg2i1fseqle  25804  itg2cnlem2  25812  dvcnv  26030  dveflem  26032  dvferm1lem  26037  dvlip2  26049  c1liplem1  26050  dvivthlem1  26062  lhop1lem  26067  dvcvx  26074  dvfsumle  26075  dvfsumleOLD  26076  dvfsumabs  26078  dvfsumlem4  26085  dvfsumrlim2  26088  ftc1a  26093  tdeglem4  26114  deg1pwle  26174  fta1blem  26225  aalioulem3  26391  aaliou2b  26398  ulmbdd  26456  ulmdvlem1  26458  itgulm  26466  pserdvlem2  26487  abelthlem3  26492  abelthlem5  26494  abelthlem6  26495  abelthlem7  26497  tanregt0  26596  argimlt0  26670  logdivlti  26677  logcnlem3  26701  logcnlem4  26702  logtayl  26717  logtayl2  26719  cxple2  26754  cxpcn3lem  26805  cxpaddle  26810  rtprmirr  26818  isosctrlem1  26876  atantayl  26995  efrlim  27027  efrlimOLD  27028  dfef2  27029  o1cxp  27033  cxp2lim  27035  divsqrtsumo1  27042  amgmlem  27048  logdifbnd  27052  emcllem7  27060  harmonicbnd4  27069  fsumharmonic  27070  lgamgulmlem2  27088  lgamgulmlem3  27089  lgamucov  27096  lgamcvg2  27113  gamcvg2  27118  ftalem2  27132  basellem2  27140  basellem5  27143  basellem9  27147  vma1  27224  sqff1o  27240  fsumfldivdiaglem  27247  chtub  27271  fsumvma2  27273  chpchtsum  27278  chpub  27279  logfaclbnd  27281  logfacbnd3  27282  logfacrlim  27283  logexprlim  27284  bcmono  27336  bposlem2  27344  bposlem5  27347  bposlem6  27348  lgsne0  27394  lgsquadlem1  27439  lgsquadlem2  27440  2sqblem  27490  2sqmod  27495  chebbnd1lem1  27528  chtppilimlem1  27532  chtppilimlem2  27533  chpchtlim  27538  rplogsumlem1  27543  dchrvmasumiflem1  27560  dchrisum0flblem2  27568  dchrisum0fno1  27570  dchrisum0lem2a  27576  dchrisum0lem3  27578  dirith  27588  mulog2sumlem1  27593  mulog2sumlem2  27594  log2sumbnd  27603  selberglem2  27605  logdivbnd  27615  selberg3lem1  27616  selberg4lem1  27619  pntrsumbnd2  27626  pntrlog2bndlem1  27636  pntrlog2bndlem5  27640  pntrlog2bndlem6  27642  pntpbnd1a  27644  pntpbnd1  27645  pntpbnd2  27646  pntibndlem3  27651  pntlemb  27656  pntlemn  27659  pntlemr  27661  pntlemj  27662  pntlemf  27664  pntlemo  27666  ostth2lem3  27694  ostth3  27697  addsuniflem  28049  sltp1d  28063  negsid  28088  negsunif  28102  mulsuniflem  28190  precsexlem9  28254  om2noseqlt  28320  n0sge0  28356  zscut  28408  addhalfcut  28434  footeq  28747  hlperpnel  28748  perpdragALT  28750  perpdrag  28751  colperp  28752  mideulem2  28757  opphllem  28758  opphllem3  28772  lmieu  28807  trgcopy  28827  sacgr  28854  acopyeu  28857  usgredgleordALT  29266  eucrctshift  30272  nvabs  30701  smcnlem  30726  ubthlem2  30900  minvecolem4  30909  htthlem  30946  normpyc  31175  nmophmi  32060  hstle  32259  hstles  32260  stlei  32269  f1rnen  32646  nnmulge  32756  fsumiunle  32836  wrdt2ind  32923  xrge0npcan  33008  gsumwrd2dccat  33053  trsp2cyc  33126  archirngz  33179  archiabllem1a  33181  archiabllem2a  33184  archiabllem2c  33185  elrgspnlem1  33232  ornglmulle  33315  orngrmulle  33316  rprmasso  33533  q1pdir  33603  r1pquslmic  33611  drngdimgt0  33646  lbsdiflsp0  33654  minplyirredlem  33718  madjusmdetlem2  33789  esumpinfval  34054  esumpinfsum  34058  esumpcvgval  34059  esum2d  34074  esumiun  34075  dya2icoseg  34259  omssubadd  34282  carsgsigalem  34297  carsggect  34300  carsgclctunlem3  34302  omsmeas  34305  eulerpartlems  34342  sgnmulsgn  34531  signsplypnf  34544  signsply0  34545  reprlt  34613  reprinfz1  34616  hgt750lemc  34641  hgt750lemf  34647  pthhashvtx  35112  resconn  35231  sinccvglem  35657  circum  35659  btwnxfr  36038  nn0prpwlem  36305  dnibndlem2  36462  unblimceq0  36490  irrdiff  37309  poimirlem7  37614  mblfinlem3  37646  mblfinlem4  37647  itg2addnclem3  37660  ftc1anc  37688  isbnd3  37771  cntotbnd  37783  bfp  37811  rrndstprj2  37818  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  42029  lcmineqlem20  42030  aks4d1p1p5  42057  aks4d1p8d2  42067  aks4d1p8  42069  aks4d1p9  42070  hashscontpow  42104  metakunt29  42215  2xp3dxp2ge1d  42223  factwoffsmonot  42224  dvdsexpnn  42347  selvvvval  42572  evlselv  42574  mhphflem  42583  fltnlta  42650  3cubeslem1  42672  irrapxlem1  42810  irrapxlem4  42813  pell1qrgaplem  42861  pellfundglb  42873  rmspecfund  42897  monotoddzzfi  42931  rmynn  42945  jm2.24nn  42948  jm2.17c  42951  jm2.24  42952  acongeq  42972  jm2.20nn  42986  jm2.26lem3  42990  jm2.27a  42994  jm2.27c  42996  rmydioph  43003  jm3.1lem2  43007  frlmpwfi  43087  areaquad  43205  cantnf2  43315  rp-isfinite6  43508  frege129d  43753  leeq1d  44147  imo72b2lem0  44155  imo72b2  44162  cvgdvgrat  44309  radcnvrat  44310  hashnzfzclim  44318  isosctrlem1ALT  44932  cncmpmax  44970  iooabslt  45452  fmul01lt1lem2  45541  clim1fr1  45557  limcrecl  45585  climxrrelem  45705  liminflbuz2  45771  dvnprodlem1  45902  stoweidlem1  45957  stoweidlem11  45967  stoweidlem14  45970  stoweidlem24  45980  stoweidlem26  45982  wallispilem4  46024  wallispilem5  46025  stirlinglem1  46030  fourierdlem51  46113  fourierdlem65  46127  fouriersw  46187  2leaddle2  47248  sqrtpwpw2p  47463  lighneallem4a  47533  flnn0div2ge  48383  logbpw2m1  48417  amgmwlem  49033