Theorem eqbrtrrd 5171

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5147

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  dftpos4  8232  dif1en  9162  dif1enOLD  9164  fodomfi  9327  fmptssfisupp  9391  resfifsupp  9394  cnfcom2lem  9698  dmttrcl  9718  ttrclselem2  9723  ficardadju  10196  enfin1ai  10381  pwcfsdom  10580  fpwwe2lem6  10633  fpwwe2  10640  canthp1lem1  10649  1nqenq  10959  prlem936  11044  lemulge11  12080  supaddc  12185  supmul1  12187  mul2lt0llt0  13082  mul2lt0lgt0  13083  xaddge0  13241  xadddi2  13280  ltexp2a  14135  leexp2a  14141  nnlesq  14173  digit1  14204  faclbnd4lem1  14257  faclbnd6  14263  facavg  14265  prsshashgt1  14374  nehash2  14439  abs3dif  15282  abs2dif  15283  limsupgre  15429  rlimclim1  15493  rlimuni  15498  rlimres2  15509  rlimcn1  15536  rlimcn1b  15537  recn2  15549  imcn2  15550  rlimo1  15565  o1rlimmul  15567  iserex  15607  isercoll  15618  caucvgrlem2  15625  caucvgr  15626  iseraltlem3  15634  summolem2a  15665  fsumge1  15747  o1fsum  15763  isumrpcl  15793  climcnds  15801  harmonic  15809  mertenslem1  15834  prodmolem2a  15882  ege2le3  16037  efgt1p2  16061  efgt1p  16062  eirrlem  16151  rpnnen2lem11  16171  fsumdvds  16255  bitsfzo  16380  bitsmod  16381  bitscmp  16383  mulgcd  16494  dvdssqlem  16507  nn0seqcvgd  16511  mulgcddvds  16596  rpdvds  16601  qden1elz  16697  phimullem  16716  hashgcdlem  16725  hashgcdeq  16726  pcdvdstr  16813  pockthg  16843  prmreclem1  16853  4sqlem11  16892  ramub1lem1  16963  ramub1lem2  16964  mreexexlem4d  17595  sscid  17775  latmlej21  18437  latmlej22  18438  lubel  18471  efginvrel1  19637  odadd2  19758  odadd  19759  gexexlem  19761  cyggex2  19806  ablfacrplem  19976  ablfac1c  19982  ablfac1eu  19984  pgpfac1lem3a  19987  isabvd  20571  mptscmfsuppd  20682  znrrg  21340  frlmphl  21555  frlmup1  21572  f1linds  21599  chcoeffeqlem  22607  lmcn2  23373  metrtri  24083  imasdsf1olem  24099  stdbdxmet  24244  nrmmetd  24303  nmmtri  24351  nlmvscnlem2  24422  blcvx  24534  recld2  24550  zdis  24552  opnreen  24567  cnheibor  24701  lebnumlem3  24709  nmoleub2lem3  24862  nmoleub2lem2  24863  nmoleub3  24866  ipcnlem2  24992  cmetcaulem  25036  nglmle  25050  cncmet  25070  csbren  25147  trirn  25148  minveclem4  25180  ovoliunlem1  25251  ovoliun2  25255  ovolscalem1  25262  ovolicopnf  25273  voliunlem2  25300  volsup  25305  ioorcl2  25321  uniiccvol  25329  uniioombllem4  25335  i1fd  25430  mbfi1fseqlem4  25468  itg2const2  25491  itg2eqa  25495  itg2split  25499  itg2i1fseqle  25504  itg2cnlem2  25512  dvcnv  25729  dveflem  25731  dvferm1lem  25736  dvlip2  25747  c1liplem1  25748  dvivthlem1  25760  lhop1lem  25765  dvcvx  25772  dvfsumle  25773  dvfsumabs  25775  dvfsumlem4  25781  dvfsumrlim2  25784  ftc1a  25789  tdeglem4  25812  tdeglem4OLD  25813  deg1pwle  25872  fta1blem  25921  aalioulem3  26083  aaliou2b  26090  ulmbdd  26146  ulmdvlem1  26148  itgulm  26156  pserdvlem2  26176  abelthlem3  26181  abelthlem5  26183  abelthlem6  26184  abelthlem7  26186  tanregt0  26284  argimlt0  26357  logdivlti  26364  logcnlem3  26388  logcnlem4  26389  logtayl  26404  logtayl2  26406  cxple2  26441  cxpcn3lem  26491  cxpaddle  26496  isosctrlem1  26559  atantayl  26678  efrlim  26710  dfef2  26711  o1cxp  26715  cxp2lim  26717  divsqrtsumo1  26724  amgmlem  26730  logdifbnd  26734  emcllem7  26742  harmonicbnd4  26751  fsumharmonic  26752  lgamgulmlem2  26770  lgamgulmlem3  26771  lgamucov  26778  lgamcvg2  26795  gamcvg2  26800  ftalem2  26814  basellem2  26822  basellem5  26825  basellem9  26829  vma1  26906  sqff1o  26922  fsumfldivdiaglem  26929  chtub  26951  fsumvma2  26953  chpchtsum  26958  chpub  26959  logfaclbnd  26961  logfacbnd3  26962  logfacrlim  26963  logexprlim  26964  bcmono  27016  bposlem2  27024  bposlem5  27027  bposlem6  27028  lgsne0  27074  lgsquadlem1  27119  lgsquadlem2  27120  2sqblem  27170  2sqmod  27175  chebbnd1lem1  27208  chtppilimlem1  27212  chtppilimlem2  27213  chpchtlim  27218  rplogsumlem1  27223  dchrvmasumiflem1  27240  dchrisum0flblem2  27248  dchrisum0fno1  27250  dchrisum0lem2a  27256  dchrisum0lem3  27258  dirith  27268  mulog2sumlem1  27273  mulog2sumlem2  27274  log2sumbnd  27283  selberglem2  27285  logdivbnd  27295  selberg3lem1  27296  selberg4lem1  27299  pntrsumbnd2  27306  pntrlog2bndlem1  27316  pntrlog2bndlem5  27320  pntrlog2bndlem6  27322  pntpbnd1a  27324  pntpbnd1  27325  pntpbnd2  27326  pntibndlem3  27331  pntlemb  27336  pntlemn  27339  pntlemr  27341  pntlemj  27342  pntlemf  27344  pntlemo  27346  ostth2lem3  27374  ostth3  27377  addsuniflem  27723  negsid  27754  negsunif  27768  mulsuniflem  27843  precsexlem9  27900  footeq  28242  hlperpnel  28243  perpdragALT  28245  perpdrag  28246  colperp  28247  mideulem2  28252  opphllem  28253  opphllem3  28267  lmieu  28302  trgcopy  28322  sacgr  28349  acopyeu  28352  usgredgleordALT  28758  eucrctshift  29763  nvabs  30192  smcnlem  30217  ubthlem2  30391  minvecolem4  30400  htthlem  30437  normpyc  30666  nmophmi  31551  hstle  31750  hstles  31751  stlei  31760  f1rnen  32120  nnmulge  32230  fsumiunle  32302  wrdt2ind  32384  xrge0npcan  32462  trsp2cyc  32552  archirngz  32605  archiabllem1a  32607  archiabllem2a  32610  archiabllem2c  32611  ornglmulle  32693  orngrmulle  32694  q1pdir  32948  r1pquslmic  32956  drngdimgt0  32991  lbsdiflsp0  32999  minplyirredlem  33058  madjusmdetlem2  33106  esumpinfval  33369  esumpinfsum  33373  esumpcvgval  33374  esum2d  33389  esumiun  33390  dya2icoseg  33574  omssubadd  33597  carsgsigalem  33612  carsggect  33615  carsgclctunlem3  33617  omsmeas  33620  eulerpartlems  33657  sgnmulsgn  33846  signsplypnf  33859  signsply0  33860  reprlt  33929  reprinfz1  33932  hgt750lemc  33957  hgt750lemf  33963  pthhashvtx  34416  resconn  34535  sinccvglem  34955  circum  34957  btwnxfr  35332  gg-dvfsumle  35468  nn0prpwlem  35510  dnibndlem2  35658  unblimceq0  35686  irrdiff  36510  poimirlem7  36798  mblfinlem3  36830  mblfinlem4  36831  itg2addnclem3  36844  ftc1anc  36872  isbnd3  36955  cntotbnd  36967  bfp  36995  rrndstprj2  37002  1cvrjat  38649  3atlem1  38657  3atlem6  38662  llnmlplnN  38713  2llnjaN  38740  2lplnja  38793  dalem57  38903  dalawlem11  39055  dalawlem12  39056  lhp2lt  39175  lhpj1  39196  lhpm0atN  39203  4atexlemex2  39245  lautm  39268  cdleme17b  39461  cdleme20j  39492  cdleme30a  39552  cdlemg4c  39786  cdlemg17a  39835  cdlemg31c  39873  trljco  39914  cdlemk46  40122  dia2dimlem2  40239  cdlemm10N  40292  cdlemn10  40380  dihmeetlem1N  40464  dihglblem5apreN  40465  dihmeetlem15N  40495  mapdat  40841  lcmineqlem19  41218  lcmineqlem20  41219  aks4d1p1p5  41246  aks4d1p8d2  41256  aks4d1p8  41258  aks4d1p9  41259  metakunt29  41319  2xp3dxp2ge1d  41328  factwoffsmonot  41329  selvvvval  41459  evlselv  41461  mhphflem  41470  dvdsexpnn  41533  rtprmirr  41539  fltnlta  41707  3cubeslem1  41724  irrapxlem1  41862  irrapxlem4  41865  pell1qrgaplem  41913  pellfundglb  41925  rmspecfund  41949  monotoddzzfi  41983  rmynn  41997  jm2.24nn  42000  jm2.17c  42003  jm2.24  42004  acongeq  42024  jm2.20nn  42038  jm2.26lem3  42042  jm2.27a  42046  jm2.27c  42048  rmydioph  42055  jm3.1lem2  42059  frlmpwfi  42142  areaquad  42267  cantnf2  42377  rp-isfinite6  42571  frege129d  42816  leeq1d  43210  imo72b2  43226  cvgdvgrat  43374  radcnvrat  43375  hashnzfzclim  43383  isosctrlem1ALT  43997  cncmpmax  44018  iooabslt  44510  fmul01lt1lem2  44599  clim1fr1  44615  limcrecl  44643  climxrrelem  44763  liminflbuz2  44829  stoweidlem1  45015  stoweidlem11  45025  stoweidlem14  45028  stoweidlem24  45038  stoweidlem26  45040  wallispilem4  45082  wallispilem5  45083  stirlinglem1  45088  fourierdlem51  45171  fourierdlem65  45185  fouriersw  45245  2leaddle2  46304  sqrtpwpw2p  46504  lighneallem4a  46574  flnn0div2ge  47306  logbpw2m1  47340  amgmwlem  47936