Theorem eqbrtrrd 5190

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  dftpos4  8286  dif1en  9226  dif1enOLD  9228  fodomfi  9378  fodomfiOLD  9398  fmptssfisupp  9463  resfifsupp  9466  cnfcom2lem  9770  dmttrcl  9790  ttrclselem2  9795  ficardadju  10269  enfin1ai  10453  pwcfsdom  10652  fpwwe2lem6  10705  fpwwe2  10712  canthp1lem1  10721  1nqenq  11031  prlem936  11116  lemulge11  12157  supaddc  12262  supmul1  12264  mul2lt0llt0  13161  mul2lt0lgt0  13162  xaddge0  13320  xadddi2  13359  ltexp2a  14216  leexp2a  14222  nnlesq  14254  digit1  14286  faclbnd4lem1  14342  faclbnd6  14348  facavg  14350  prsshashgt1  14459  nehash2  14523  abs3dif  15380  abs2dif  15381  limsupgre  15527  rlimclim1  15591  rlimuni  15596  rlimres2  15607  rlimcn1  15634  rlimcn1b  15635  recn2  15647  imcn2  15648  rlimo1  15663  o1rlimmul  15665  iserex  15705  isercoll  15716  caucvgrlem2  15723  caucvgr  15724  iseraltlem3  15732  summolem2a  15763  fsumge1  15845  o1fsum  15861  isumrpcl  15891  climcnds  15899  harmonic  15907  mertenslem1  15932  prodmolem2a  15982  ege2le3  16138  efgt1p2  16162  efgt1p  16163  eirrlem  16252  rpnnen2lem11  16272  fsumdvds  16356  bitsfzo  16481  bitsmod  16482  bitscmp  16484  mulgcd  16595  dvdssqlem  16613  nn0seqcvgd  16617  mulgcddvds  16702  rpdvds  16707  qden1elz  16804  phimullem  16826  hashgcdlem  16835  hashgcdeq  16836  pcdvdstr  16923  pockthg  16953  prmreclem1  16963  4sqlem11  17002  ramub1lem1  17073  ramub1lem2  17074  mreexexlem4d  17705  sscid  17885  latmlej21  18550  latmlej22  18551  lubel  18584  efginvrel1  19770  odadd2  19891  odadd  19892  gexexlem  19894  cyggex2  19939  ablfacrplem  20109  ablfac1c  20115  ablfac1eu  20117  pgpfac1lem3a  20120  isabvd  20835  mptscmfsuppd  20948  znrrg  21607  frlmphl  21824  frlmup1  21841  f1linds  21868  psdmplcl  22189  chcoeffeqlem  22912  lmcn2  23678  metrtri  24388  imasdsf1olem  24404  stdbdxmet  24549  nrmmetd  24608  nmmtri  24656  nlmvscnlem2  24727  blcvx  24839  recld2  24855  zdis  24857  opnreen  24872  cnheibor  25006  lebnumlem3  25014  nmoleub2lem3  25167  nmoleub2lem2  25168  nmoleub3  25171  ipcnlem2  25297  cmetcaulem  25341  nglmle  25355  cncmet  25375  csbren  25452  trirn  25453  minveclem4  25485  ovoliunlem1  25556  ovoliun2  25560  ovolscalem1  25567  ovolicopnf  25578  voliunlem2  25605  volsup  25610  ioorcl2  25626  uniiccvol  25634  uniioombllem4  25640  i1fd  25735  mbfi1fseqlem4  25773  itg2const2  25796  itg2eqa  25800  itg2split  25804  itg2i1fseqle  25809  itg2cnlem2  25817  dvcnv  26035  dveflem  26037  dvferm1lem  26042  dvlip2  26054  c1liplem1  26055  dvivthlem1  26067  lhop1lem  26072  dvcvx  26079  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem4  26090  dvfsumrlim2  26093  ftc1a  26098  tdeglem4  26119  deg1pwle  26179  fta1blem  26230  aalioulem3  26394  aaliou2b  26401  ulmbdd  26459  ulmdvlem1  26461  itgulm  26469  pserdvlem2  26490  abelthlem3  26495  abelthlem5  26497  abelthlem6  26498  abelthlem7  26500  tanregt0  26599  argimlt0  26673  logdivlti  26680  logcnlem3  26704  logcnlem4  26705  logtayl  26720  logtayl2  26722  cxple2  26757  cxpcn3lem  26808  cxpaddle  26813  rtprmirr  26821  isosctrlem1  26879  atantayl  26998  efrlim  27030  efrlimOLD  27031  dfef2  27032  o1cxp  27036  cxp2lim  27038  divsqrtsumo1  27045  amgmlem  27051  logdifbnd  27055  emcllem7  27063  harmonicbnd4  27072  fsumharmonic  27073  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamucov  27099  lgamcvg2  27116  gamcvg2  27121  ftalem2  27135  basellem2  27143  basellem5  27146  basellem9  27150  vma1  27227  sqff1o  27243  fsumfldivdiaglem  27250  chtub  27274  fsumvma2  27276  chpchtsum  27281  chpub  27282  logfaclbnd  27284  logfacbnd3  27285  logfacrlim  27286  logexprlim  27287  bcmono  27339  bposlem2  27347  bposlem5  27350  bposlem6  27351  lgsne0  27397  lgsquadlem1  27442  lgsquadlem2  27443  2sqblem  27493  2sqmod  27498  chebbnd1lem1  27531  chtppilimlem1  27535  chtppilimlem2  27536  chpchtlim  27541  rplogsumlem1  27546  dchrvmasumiflem1  27563  dchrisum0flblem2  27571  dchrisum0fno1  27573  dchrisum0lem2a  27579  dchrisum0lem3  27581  dirith  27591  mulog2sumlem1  27596  mulog2sumlem2  27597  log2sumbnd  27606  selberglem2  27608  logdivbnd  27618  selberg3lem1  27619  selberg4lem1  27622  pntrsumbnd2  27629  pntrlog2bndlem1  27639  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntpbnd1a  27647  pntpbnd1  27648  pntpbnd2  27649  pntibndlem3  27654  pntlemb  27659  pntlemn  27662  pntlemr  27664  pntlemj  27665  pntlemf  27667  pntlemo  27669  ostth2lem3  27697  ostth3  27700  addsuniflem  28052  sltp1d  28066  negsid  28091  negsunif  28105  mulsuniflem  28193  precsexlem9  28257  om2noseqlt  28323  n0sge0  28359  zscut  28411  addhalfcut  28437  footeq  28750  hlperpnel  28751  perpdragALT  28753  perpdrag  28754  colperp  28755  mideulem2  28760  opphllem  28761  opphllem3  28775  lmieu  28810  trgcopy  28830  sacgr  28857  acopyeu  28860  usgredgleordALT  29269  eucrctshift  30275  nvabs  30704  smcnlem  30729  ubthlem2  30903  minvecolem4  30912  htthlem  30949  normpyc  31178  nmophmi  32063  hstle  32262  hstles  32263  stlei  32272  f1rnen  32648  nnmulge  32752  fsumiunle  32833  wrdt2ind  32920  xrge0npcan  33006  trsp2cyc  33116  archirngz  33169  archiabllem1a  33171  archiabllem2a  33174  archiabllem2c  33175  ornglmulle  33300  orngrmulle  33301  rprmasso  33518  q1pdir  33588  r1pquslmic  33596  drngdimgt0  33631  lbsdiflsp0  33639  minplyirredlem  33703  madjusmdetlem2  33774  esumpinfval  34037  esumpinfsum  34041  esumpcvgval  34042  esum2d  34057  esumiun  34058  dya2icoseg  34242  omssubadd  34265  carsgsigalem  34280  carsggect  34283  carsgclctunlem3  34285  omsmeas  34288  eulerpartlems  34325  sgnmulsgn  34514  signsplypnf  34527  signsply0  34528  reprlt  34596  reprinfz1  34599  hgt750lemc  34624  hgt750lemf  34630  pthhashvtx  35095  resconn  35214  sinccvglem  35640  circum  35642  btwnxfr  36020  nn0prpwlem  36288  dnibndlem2  36445  unblimceq0  36473  irrdiff  37292  poimirlem7  37587  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem3  37633  ftc1anc  37661  isbnd3  37744  cntotbnd  37756  bfp  37784  rrndstprj2  37791  1cvrjat  39432  3atlem1  39440  3atlem6  39445  llnmlplnN  39496  2llnjaN  39523  2lplnja  39576  dalem57  39686  dalawlem11  39838  dalawlem12  39839  lhp2lt  39958  lhpj1  39979  lhpm0atN  39986  4atexlemex2  40028  lautm  40051  cdleme17b  40244  cdleme20j  40275  cdleme30a  40335  cdlemg4c  40569  cdlemg17a  40618  cdlemg31c  40656  trljco  40697  cdlemk46  40905  dia2dimlem2  41022  cdlemm10N  41075  cdlemn10  41163  dihmeetlem1N  41247  dihglblem5apreN  41248  dihmeetlem15N  41278  mapdat  41624  lcmineqlem19  42004  lcmineqlem20  42005  aks4d1p1p5  42032  aks4d1p8d2  42042  aks4d1p8  42044  aks4d1p9  42045  hashscontpow  42079  metakunt29  42190  2xp3dxp2ge1d  42198  factwoffsmonot  42199  dvdsexpnn  42320  selvvvval  42540  evlselv  42542  mhphflem  42551  fltnlta  42618  3cubeslem1  42640  irrapxlem1  42778  irrapxlem4  42781  pell1qrgaplem  42829  pellfundglb  42841  rmspecfund  42865  monotoddzzfi  42899  rmynn  42913  jm2.24nn  42916  jm2.17c  42919  jm2.24  42920  acongeq  42940  jm2.20nn  42954  jm2.26lem3  42958  jm2.27a  42962  jm2.27c  42964  rmydioph  42971  jm3.1lem2  42975  frlmpwfi  43055  areaquad  43177  cantnf2  43287  rp-isfinite6  43480  frege129d  43725  leeq1d  44119  imo72b2  44134  cvgdvgrat  44282  radcnvrat  44283  hashnzfzclim  44291  isosctrlem1ALT  44905  cncmpmax  44932  iooabslt  45417  fmul01lt1lem2  45506  clim1fr1  45522  limcrecl  45550  climxrrelem  45670  liminflbuz2  45736  stoweidlem1  45922  stoweidlem11  45932  stoweidlem14  45935  stoweidlem24  45945  stoweidlem26  45947  wallispilem4  45989  wallispilem5  45990  stirlinglem1  45995  fourierdlem51  46078  fourierdlem65  46092  fouriersw  46152  2leaddle2  47213  sqrtpwpw2p  47412  lighneallem4a  47482  flnn0div2ge  48267  logbpw2m1  48301  amgmwlem  48896