Theorem eqbrtrrd 5090

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  dftpos4  7911  fodomfi  8797  resfifsupp  8861  cnfcom2lem  9164  enfin1ai  9806  pwcfsdom  10005  fpwwe2lem7  10058  fpwwe2  10065  canthp1lem1  10074  1nqenq  10384  prlem936  10469  lemulge11  11502  supaddc  11608  supmul1  11610  mul2lt0llt0  12494  mul2lt0lgt0  12495  xaddge0  12652  xadddi2  12691  ltexp2a  13531  leexp2a  13537  nnlesq  13569  digit1  13599  faclbnd4lem1  13654  faclbnd6  13660  facavg  13662  prsshashgt1  13772  nehash2  13833  abs3dif  14691  abs2dif  14692  limsupgre  14838  rlimclim1  14902  rlimuni  14907  rlimres2  14918  rlimcn1  14945  rlimcn1b  14946  recn2  14957  imcn2  14958  rlimo1  14973  o1rlimmul  14975  iserex  15013  isercoll  15024  caucvgrlem2  15031  caucvgr  15032  iseraltlem3  15040  summolem2a  15072  fsumge1  15152  o1fsum  15168  isumrpcl  15198  climcnds  15206  harmonic  15214  mertenslem1  15240  prodmolem2a  15288  ege2le3  15443  efgt1p2  15467  efgt1p  15468  eirrlem  15557  rpnnen2lem11  15577  fsumdvds  15658  bitsfzo  15784  bitsmod  15785  bitscmp  15787  mulgcd  15896  dvdssqlem  15910  nn0seqcvgd  15914  mulgcddvds  15999  rpdvds  16004  qden1elz  16097  phimullem  16116  hashgcdlem  16125  hashgcdeq  16126  pcdvdstr  16212  pockthg  16242  prmreclem1  16252  4sqlem11  16291  ramub1lem1  16362  ramub1lem2  16363  mreexexlem4d  16918  sscid  17094  latmlej21  17702  latmlej22  17703  lubel  17732  efginvrel1  18854  odadd2  18969  odadd  18970  gexexlem  18972  cyggex2  19017  ablfacrplem  19187  ablfac1c  19193  ablfac1eu  19195  pgpfac1lem3a  19198  isabvd  19591  mptscmfsuppd  19700  znrrg  20712  frlmphl  20925  frlmup1  20942  f1linds  20969  chcoeffeqlem  21493  lmcn2  22257  metrtri  22967  imasdsf1olem  22983  stdbdxmet  23125  nrmmetd  23184  nmmtri  23231  nlmvscnlem2  23294  blcvx  23406  recld2  23422  zdis  23424  opnreen  23439  cnheibor  23559  lebnumlem3  23567  nmoleub2lem3  23719  nmoleub2lem2  23720  nmoleub3  23723  ipcnlem2  23847  cmetcaulem  23891  nglmle  23905  cncmet  23925  csbren  24002  trirn  24003  minveclem4  24035  ovoliunlem1  24103  ovoliun2  24107  ovolscalem1  24114  ovolicopnf  24125  voliunlem2  24152  volsup  24157  ioorcl2  24173  uniiccvol  24181  uniioombllem4  24187  i1fd  24282  mbfi1fseqlem4  24319  itg2const2  24342  itg2eqa  24346  itg2split  24350  itg2i1fseqle  24355  itg2cnlem2  24363  dvcnv  24574  dveflem  24576  dvferm1lem  24581  dvlip2  24592  c1liplem1  24593  dvivthlem1  24605  lhop1lem  24610  dvcvx  24617  dvfsumle  24618  dvfsumabs  24620  dvfsumlem4  24626  dvfsumrlim2  24629  ftc1a  24634  tdeglem4  24654  deg1pwle  24713  fta1blem  24762  aalioulem3  24923  aaliou2b  24930  ulmbdd  24986  ulmdvlem1  24988  itgulm  24996  pserdvlem2  25016  abelthlem3  25021  abelthlem5  25023  abelthlem6  25024  abelthlem7  25026  tanregt0  25123  argimlt0  25196  logdivlti  25203  logcnlem3  25227  logcnlem4  25228  logtayl  25243  logtayl2  25245  cxple2  25280  cxpcn3lem  25328  cxpaddle  25333  isosctrlem1  25396  atantayl  25515  efrlim  25547  dfef2  25548  o1cxp  25552  cxp2lim  25554  divsqrtsumo1  25561  amgmlem  25567  logdifbnd  25571  emcllem7  25579  harmonicbnd4  25588  fsumharmonic  25589  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamucov  25615  lgamcvg2  25632  gamcvg2  25637  ftalem2  25651  basellem2  25659  basellem5  25662  basellem9  25666  vma1  25743  sqff1o  25759  fsumfldivdiaglem  25766  chtub  25788  fsumvma2  25790  chpchtsum  25795  chpub  25796  logfaclbnd  25798  logfacbnd3  25799  logfacrlim  25800  logexprlim  25801  bcmono  25853  bposlem2  25861  bposlem5  25864  bposlem6  25865  lgsne0  25911  lgsquadlem1  25956  lgsquadlem2  25957  2sqblem  26007  2sqmod  26012  chebbnd1lem1  26045  chtppilimlem1  26049  chtppilimlem2  26050  chpchtlim  26055  rplogsumlem1  26060  dchrvmasumiflem1  26077  dchrisum0flblem2  26085  dchrisum0fno1  26087  dchrisum0lem2a  26093  dchrisum0lem3  26095  dirith  26105  mulog2sumlem1  26110  mulog2sumlem2  26111  log2sumbnd  26120  selberglem2  26122  logdivbnd  26132  selberg3lem1  26133  selberg4lem1  26136  pntrsumbnd2  26143  pntrlog2bndlem1  26153  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntibndlem3  26168  pntlemb  26173  pntlemn  26176  pntlemr  26178  pntlemj  26179  pntlemf  26181  pntlemo  26183  ostth2lem3  26211  ostth3  26214  footeq  26510  hlperpnel  26511  perpdragALT  26513  perpdrag  26514  colperp  26515  mideulem2  26520  opphllem  26521  opphllem3  26535  lmieu  26570  trgcopy  26590  sacgr  26617  acopyeu  26620  usgredgleordALT  27016  eucrctshift  28022  nvabs  28449  smcnlem  28474  ubthlem2  28648  minvecolem4  28657  htthlem  28694  normpyc  28923  nmophmi  29808  hstle  30007  hstles  30008  stlei  30017  f1rnen  30374  fmptssfisupp  30428  nnmulge  30474  fsumiunle  30545  wrdt2ind  30627  xrge0npcan  30681  trsp2cyc  30765  archirngz  30818  archiabllem1a  30820  archiabllem2a  30823  archiabllem2c  30824  ornglmulle  30878  orngrmulle  30879  drngdimgt0  31016  lbsdiflsp0  31022  madjusmdetlem2  31093  esumpinfval  31332  esumpinfsum  31336  esumpcvgval  31337  esum2d  31352  esumiun  31353  dya2icoseg  31535  omssubadd  31558  carsgsigalem  31573  carsggect  31576  carsgclctunlem3  31578  omsmeas  31581  eulerpartlems  31618  sgnmulsgn  31807  signsplypnf  31820  signsply0  31821  reprlt  31890  reprinfz1  31893  hgt750lemc  31918  hgt750lemf  31924  pthhashvtx  32374  resconn  32493  sinccvglem  32915  circum  32917  btwnxfr  33517  nn0prpwlem  33670  dnibndlem2  33818  unblimceq0  33846  poimirlem7  34914  mblfinlem3  34946  mblfinlem4  34947  itg2addnclem3  34960  ftc1anc  34990  isbnd3  35077  cntotbnd  35089  bfp  35117  rrndstprj2  35124  1cvrjat  36626  3atlem1  36634  3atlem6  36639  llnmlplnN  36690  2llnjaN  36717  2lplnja  36770  dalem57  36880  dalawlem11  37032  dalawlem12  37033  lhp2lt  37152  lhpj1  37173  lhpm0atN  37180  4atexlemex2  37222  lautm  37245  cdleme17b  37438  cdleme20j  37469  cdleme30a  37529  cdlemg4c  37763  cdlemg17a  37812  cdlemg31c  37850  trljco  37891  cdlemk46  38099  dia2dimlem2  38216  cdlemm10N  38269  cdlemn10  38357  dihmeetlem1N  38441  dihglblem5apreN  38442  dihmeetlem15N  38472  mapdat  38818  2xp3dxp2ge1d  39146  factwoffsmonot  39147  rtprmirr  39243  fltnlta  39324  3cubeslem1  39330  irrapxlem1  39468  irrapxlem4  39471  pell1qrgaplem  39519  pellfundglb  39531  rmspecfund  39555  monotoddzzfi  39588  rmynn  39602  jm2.24nn  39605  jm2.17c  39608  jm2.24  39609  acongeq  39629  jm2.20nn  39643  jm2.26lem3  39647  jm2.27a  39651  jm2.27c  39653  rmydioph  39660  jm3.1lem2  39664  frlmpwfi  39747  areaquad  39872  rp-isfinite6  39933  frege129d  40157  leeq1d  40556  imo72b2  40574  cvgdvgrat  40694  radcnvrat  40695  hashnzfzclim  40703  isosctrlem1ALT  41317  cncmpmax  41338  iooabslt  41823  fmul01lt1lem2  41915  clim1fr1  41931  limcrecl  41959  climxrrelem  42079  liminflbuz2  42145  stoweidlem1  42335  stoweidlem11  42345  stoweidlem14  42348  stoweidlem24  42358  stoweidlem26  42360  wallispilem4  42402  wallispilem5  42403  stirlinglem1  42408  fourierdlem51  42491  fourierdlem65  42505  fouriersw  42565  2leaddle2  43547  sqrtpwpw2p  43749  lighneallem4a  43822  flnn0div2ge  44642  logbpw2m1  44676  amgmwlem  44952