Theorem eqbrtrd 5097

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqbrtrd.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
eqbrtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 5085	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 256	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  eqbrtrrd  5099  somin2  6045  en1b  8822  en1bOLD  8823  domunsncan  8868  fodomfi  9101  infsupprpr  9272  hartogslem1  9310  wemaplem2  9315  infdifsn  9424  ttrclselem2  9493  carddomi2  9737  djuinf  9953  carden  10316  alephsuc3  10345  fpwwe2lem5  10400  fpwwe2lem6  10401  inar1  10540  rankcf  10542  lesub3d  11602  lbinfle  11939  supadd  11952  supmul  11956  rpnnen1lem3  12728  divge1  12807  xrmin1  12920  xrmin2  12921  ifle  12940  qbtwnxr  12943  xltnegi  12959  xleadd1a  12996  xlt2add  13003  xlemul1a  13031  xov1plusxeqvd  13239  ubmelm1fzo  13492  flflp1  13536  ceim1l  13576  ceilm1lt  13577  ceille  13579  quoremz  13584  quoremnn0ALT  13586  modlt  13609  modeqmodmin  13670  addmodlteq  13675  seqf1olem1  13771  bernneq  13953  discr  13964  faclbnd2  14014  faclbnd4lem3  14018  hashun2  14107  hashfun  14161  ccatsymb  14296  ccatrn  14303  sqrlem6  14968  sqrlem7  14969  rddif  15061  amgm2  15090  icodiamlt  15156  climconst  15261  rlimconst  15262  serclim0  15295  rlimcn1  15306  mulcn2  15314  reccn2  15315  o1mul  15333  o1rlimmul  15337  iserex  15377  climlec2  15379  iserge0  15381  climcau  15391  caucvgrlem  15393  caucvgr  15396  iseraltlem2  15403  iseraltlem3  15404  iseralt  15405  fsumabs  15522  o1fsum  15534  iserabs  15536  climfsum  15541  isumless  15566  climcndslem2  15571  divrcnv  15573  flo1  15575  supcvg  15577  georeclim  15593  geomulcvg  15597  cvgrat  15604  mertenslem1  15605  prodfclim1  15614  fprodle  15715  efcvgfsum  15804  eftlub  15827  eflegeo  15839  tanhlt1  15878  tanhbnd  15879  ef01bndlem  15902  sin01bnd  15903  cos01bnd  15904  cos01gt0  15909  ruclem2  15950  ruclem3  15951  ruclem9  15956  ruclem11  15958  ruclem12  15959  bitsfzolem  16150  bitsfzo  16151  bitsinv1lem  16157  sadcaddlem  16173  mulgcd  16265  eucalglt  16299  lcmledvds  16313  lcmfledvds  16346  mulgcddvds  16369  coprmproddvdslem  16376  prmind2  16399  isprm5  16421  divdenle  16462  nonsq  16472  pythagtriplem4  16529  pclem  16548  pcpremul  16553  pczdvds  16573  pcprmpw2  16592  qexpz  16611  prmreclem4  16629  prmreclem5  16630  4sqlem10  16657  ramtub  16722  ramub2  16724  prmodvdslcmf  16757  prmgaplem8  16768  natpropd  17703  catciso  17835  p0le  18156  acsdomd  18284  triv1nsgd  18810  qusgrp  18820  f1otrspeq  19064  pmtrfrn  19075  pmtrfconj  19083  symggen  19087  psgnunilem4  19114  oddvds2  19182  odcau  19218  pgpfi  19219  pgpssslw  19228  sylow3lem4  19244  efgred2  19368  frgp0  19375  odadd2  19459  oddvdssubg  19465  ablfac1c  19683  ablfac1eu  19685  pgpfaclem3  19695  2nsgsimpgd  19714  isabvd  20089  abvsubtri  20104  cyggic  20789  mplsubrg  21220  coe1sfi  21393  mp2pm2mplem5  21968  en2top  22144  1stcrest  22613  2ndcrest  22614  hausmapdom  22660  ufilen  23090  xmetrtri2  23518  prdsxmetlem  23530  bl2in  23562  xblcntrps  23572  xblcntr  23573  ssblps  23584  ssbl  23585  blssps  23586  blss  23587  blcld  23670  methaus  23685  metustexhalf  23721  nmtri2  23792  tngngp3  23829  nrginvrcnlem  23864  nrginvrcn  23865  nmoi  23901  nmo0  23908  nmoid  23915  blcvx  23970  reperflem  23990  reconnlem2  23999  metdcnlem  24008  metdscn  24028  metnrmlem3  24033  mulc1cncf  24077  iccpnfhmeo  24117  cnheiborlem  24126  cnheibor  24127  lebnumii  24138  pcopt  24194  pcopt2  24195  pcoass  24196  nmoleub2lem  24286  nmoleub2lem3  24287  nmoleub2lem2  24288  ipcau2  24407  tcphcphlem1  24408  nglmle  24475  trirn  24573  rrxdstprj1  24582  minveclem3  24602  ivthlem2  24625  ivthlem3  24626  ivth2  24628  ovollb  24652  ovolsslem  24657  ovollb2lem  24661  ovolctb  24663  ovoliunlem1  24675  ovolsca  24688  ovolicc1  24689  ovolicc2lem4  24693  nulmbl  24708  ioombl1lem4  24734  uniioovol  24752  uniioombllem3a  24757  uniioombllem4  24759  opnmbllem  24774  volcn  24779  volivth  24780  i1fadd  24868  i1fmul  24869  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  mbfi1fseqlem6  24894  itg2const2  24915  itg2seq  24916  itg2uba  24917  itg2split  24923  itg2monolem1  24924  itg2monolem3  24926  itg2i1fseq2  24930  itg2addlem  24932  itg2gt0  24934  itg2cnlem1  24935  itg2cnlem2  24936  itgless  24990  ibladdlem  24993  bddmulibl  25012  dveflem  25152  dvferm1lem  25157  dvferm2lem  25159  dvlip  25166  dvlipcn  25167  dvlip2  25168  dvle  25180  dvivthlem1  25181  lhop1lem  25186  dvcvx  25193  dvfsumabs  25196  dvfsumlem2  25200  dvfsumlem4  25202  dvfsumrlim2  25205  dvfsum2  25207  ftc1a  25210  ftc1lem4  25212  ftc1lem5  25213  deg1sub  25282  ply1divex  25310  deg1submon1p  25326  r1pdeglt  25332  dvdsq1p  25334  fta1glem2  25340  fta1g  25341  plyeq0lem  25380  dgrlt  25436  fta1lem  25476  aalioulem2  25502  aalioulem3  25503  aalioulem4  25504  aaliou3lem2  25512  aaliou3lem9  25519  taylply2  25536  ulmbdd  25566  ulmdvlem1  25568  mtest  25572  mtestbdd  25573  radcnvlem1  25581  radcnvle  25588  pserulm  25590  psercn  25594  pserdvlem2  25596  abelthlem2  25600  abelthlem5  25603  abelthlem7  25606  abelthlem8  25607  abelthlem9  25608  reeff1olem  25614  tangtx  25671  tanord  25703  efif1olem4  25710  logrnaddcl  25739  logcj  25770  logimul  25778  logneg2  25779  logdivlti  25784  divlogrlim  25799  logcnlem3  25808  logcnlem4  25809  efopn  25822  logtayllem  25823  logtayl  25824  cxpcn3lem  25909  cxpaddle  25914  abscxpbnd  25915  asinlem3  26030  asinneg  26045  asinsin  26051  atanlogaddlem  26072  atantan  26082  bndatandm  26088  atans2  26090  atantayl  26096  atantayl2  26097  atantayl3  26098  leibpi  26101  birthdaylem3  26112  rlimcnp  26124  efrlim  26128  cxplim  26130  cxp2lim  26135  cxploglim2  26137  divsqrtsumo1  26142  jensenlem2  26146  amgm  26149  logdifbnd  26152  harmonicbnd4  26169  fsumharmonic  26170  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem5  26191  lgambdd  26195  lgamcvg2  26213  ftalem1  26231  ftalem5  26235  basellem1  26239  basellem8  26246  ppip1le  26319  ppiltx  26335  sqff1o  26340  chtublem  26368  chpub  26377  logfaclbnd  26379  logfacrlim  26381  logexprlim  26382  mersenne  26384  bcmono  26434  bcmax  26435  bposlem2  26442  bposlem5  26445  lgslem3  26456  gausslemma2dlem1a  26522  lgsquadlem1  26537  lgsquadlem2  26538  2lgslem1c  26550  2sqblem  26588  chebbnd1  26629  chtppilimlem1  26630  chto1ub  26633  chpchtlim  26636  chpo1ubb  26638  rplogsumlem1  26641  rplogsumlem2  26642  rpvmasumlem  26644  dchrisumlem1  26646  dchrisumlem2  26647  dchrmusum2  26651  dchrvmasumlem2  26655  dchrvmasumlem3  26656  dchrvmasumiflem1  26658  dchrisum0flblem1  26665  dchrisum0fno1  26668  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0lem2  26675  rplogsum  26684  mudivsum  26687  mulogsumlem  26688  mulog2sumlem1  26691  mulog2sumlem2  26692  vmalogdivsum2  26695  2vmadivsumlem  26697  selberglem2  26703  selberg2b  26709  logdivbnd  26713  selberg3lem1  26714  selberg3lem2  26715  selberg4lem1  26717  pntrmax  26721  pntrsumo1  26722  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntrlog2bnd  26741  pntpbnd1a  26742  pntpbnd2  26744  pntibndlem2  26748  pntlemb  26754  pntlemg  26755  pntlemh  26756  pntlemr  26759  pntlemj  26760  pntlemf  26762  pntlemo  26764  pnt  26771  padicabv  26787  ostth2lem2  26791  ostth2lem3  26792  ostth3  26795  colperpexlem3  27102  mideulem2  27104  lnperpex  27173  trgcopy  27174  iscgra1  27180  brbtwn2  27282  colinearalglem4  27286  subupgr  27663  crctcshwlkn0lem1  28184  nvabs  29043  nvge0  29044  smcnlem  29068  nmblolbii  29170  blocnilem  29175  siii  29224  ubthlem2  29242  minvecolem3  29247  htthlem  29288  bcsiALT  29550  bcs3  29554  chscllem4  30011  0cnop  30350  0cnfn  30351  nmbdoplbi  30395  nmcoplbi  30399  nmophmi  30402  nmbdfnlbi  30420  nmcfnlbi  30423  nlelchi  30432  riesz1  30436  cnlnadjlem2  30439  nmopadjlei  30459  nmoptrii  30465  nmopcoi  30466  nmopcoadji  30472  unierri  30475  branmfn  30476  pjs14i  30581  hstle  30601  cdj3lem2b  30808  xlt2addrd  31090  eliccelico  31107  elicoelioo  31108  ltesubnnd  31145  wrdt2ind  31234  archirngz  31452  archiabllem2c  31458  madjusmdetlem2  31787  locfinref  31800  sqsscirc1  31867  tpr2rico  31871  esumcst  32040  esumgect  32067  esum2d  32070  measunl  32193  measiun  32195  omssubaddlem  32275  omssubadd  32276  carsgsigalem  32291  carsgclctunlem2  32295  pmeasmono  32300  eulerpartlemgc  32338  eulerpartlemb  32344  ballotlemsel1i  32488  ballotlemro  32498  sgnsub  32520  signsplypnf  32538  signsply0  32539  signsvtn  32572  signsvfnn  32574  hgt750lemd  32637  logdivsqrle  32639  hashf1dmcdm  33085  erdsze2lem1  33174  sinccvglem  33639  divcnvlin  33707  iprodefisum  33716  faclimlem2  33719  nosep1o  33893  nodense  33904  noinfbnd2lem1  33942  noetainflem3  33951  cofcutr  34101  cofcutrtime  34102  fnemeet1  34564  dnibndlem10  34676  dnibndlem11  34677  dnibnd  34680  knoppcnlem4  34685  knoppcnlem6  34687  unblimceq0lem  34695  unbdqndv2lem1  34698  unbdqndv2lem2  34699  knoppndvlem11  34711  knoppndvlem12  34712  knoppndvlem14  34714  knoppndvlem15  34715  knoppndvlem17  34717  knoppndvlem18  34718  knoppndvlem19  34719  knoppndvlem21  34721  ctbssinf  35586  ltflcei  35774  ptrecube  35786  poimirlem16  35802  poimirlem17  35803  poimirlem29  35815  broucube  35820  opnmbllem0  35822  mblfinlem2  35824  mblfinlem3  35825  ismblfin  35827  itg2addnclem  35837  itg2addnclem2  35838  itg2addnclem3  35839  itg2addnc  35840  ibladdnclem  35842  ftc1cnnclem  35857  ftc1cnnc  35858  ftc1anc  35867  geomcau  35926  prdsbnd  35960  cntotbnd  35963  heiborlem4  35981  rrndstprj2  35998  rrncmslem  35999  rrnequiv  36002  iccbnd  36007  cvlcvr1  37360  cvrat3  37463  dalem25  37719  cdlema1N  37812  dalawlem3  37894  dalawlem4  37895  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem9  37900  dalawlem11  37902  dalawlem12  37903  lhp2lt  38022  lhpmcvr  38044  4atexlemcnd  38093  lautj  38114  trlle  38205  trlval3  38208  trlval4  38209  cdleme0moN  38246  cdleme13  38293  cdleme15  38299  cdleme19b  38325  cdleme20e  38334  cdleme20j  38339  cdleme22e  38365  cdleme22eALTN  38366  cdleme26fALTN  38383  cdleme26f  38384  cdleme27N  38390  cdleme41sn3a  38454  cdleme46fsvlpq  38526  cdlemeg46vrg  38548  cdlemg4  38638  cdlemg7N  38647  cdlemg9a  38653  cdlemg11b  38663  cdlemg12a  38664  trljco  38761  tendoidcl  38790  tendococl  38793  tendopltp  38801  tendo0tp  38810  tendoicl  38817  cdlemi2  38840  cdlemk5a  38856  cdlemk5  38857  cdlemk12  38871  cdlemkole  38874  cdlemk14  38875  cdlemk12u  38893  cdlemk37  38935  cdlemk39s-id  38961  cdlemk49  38972  cdlemk39u1  38988  cdlemk39u  38989  dian0  39060  cdlemm10N  39139  cdlemn2  39216  cdlemn10  39227  dihord1  39239  dihord10  39244  dihmeetlem4preN  39327  dihmeetlem18N  39345  dihmeetlem20N  39347  dihjatc  39438  mapdcnvatN  39687  lcmineqlem17  40060  3lexlogpow5ineq2  40070  3lexlogpow2ineq2  40074  3lexlogpow5ineq5  40075  aks4d1p1p3  40084  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p1  40091  aks4d1p3  40093  aks4d1p5  40095  aks4d1p6  40096  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8  40102  2ap1caineq  40108  sticksstones7  40115  sticksstones10  40118  sticksstones11  40119  sticksstones12a  40120  sticksstones12  40121  sticksstones22  40131  metakunt16  40147  metakunt29  40160  fltltc  40505  lzenom  40599  irrapxlem2  40652  irrapxlem3  40653  irrapxlem5  40655  pellexlem2  40659  pell14qrgt0  40688  pellfundlb  40713  pellfundex  40715  pellfund14  40727  rmspecsqrtnq  40735  jm2.24nn  40788  jm2.17a  40789  jm2.17b  40790  congabseq  40803  acongrep  40809  acongeq  40812  jm2.26lem3  40830  jm2.27a  40834  jm2.27c  40836  hbtlem2  40956  dgraaub  40980  idomodle  41028  sqrtcval  41256  relexpxpmin  41332  frege102d  41369  hashnzfzclim  41947  binomcxplemfrat  41976  binomcxplemnotnn0  41981  suprnmpt  42717  mpct  42748  rnmptbddlem  42796  dstregt0  42827  lefldiveq  42838  fzisoeu  42846  upbdrech  42851  ssfiunibd  42855  fzdifsuc2  42856  xadd0ge  42866  supxrgere  42879  supxrge  42884  suplesup  42885  xrlexaddrp  42898  infxrunb2  42914  infleinflem2  42917  reclt0d  42933  infrpgernmpt  43012  ioondisj2  43038  iccshift  43063  iooshift  43067  fmul01  43128  fmul01lt1lem1  43132  fmul01lt1lem2  43133  climrec  43151  climsuse  43156  mullimc  43164  mullimcf  43171  constlimc  43172  idlimc  43174  divcnvg  43175  limcperiod  43176  limcrecl  43177  lptioo2  43179  lptioo1  43180  islpcn  43187  lptre2pt  43188  limcleqr  43192  neglimc  43195  addlimc  43196  0ellimcdiv  43197  limclner  43199  climleltrp  43224  limsuplesup  43247  limsupmnflem  43268  supcnvlimsupmpt  43289  0cnv  43290  xlimconst  43373  xlimliminflimsup  43410  sinaover2ne0  43416  cncfshift  43422  cncfperiod  43427  cncfioobdlem  43444  cncfioobd  43445  fperdvper  43467  dvdivbd  43471  dvbdfbdioolem1  43476  dvbdfbdioolem2  43477  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnmul  43491  dvnprodlem1  43494  itgiccshift  43528  itgperiod  43529  ismbl3  43534  ovolsplit  43536  stoweidlem1  43549  stoweidlem11  43559  stoweidlem13  43561  stoweidlem14  43562  stoweidlem16  43564  stoweidlem21  43569  stoweidlem25  43573  stoweidlem26  43574  stoweidlem36  43584  stoweidlem38  43586  stoweidlem41  43589  stoweidlem42  43590  stoweidlem45  43593  stoweidlem48  43596  stoweidlem52  43600  stoweidlem62  43610  wallispilem3  43615  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem10  43631  stirlinglem12  43633  stirlinglem15  43636  dirkercncflem1  43651  fourierdlem10  43665  fourierdlem12  43667  fourierdlem15  43670  fourierdlem16  43671  fourierdlem19  43674  fourierdlem20  43675  fourierdlem21  43676  fourierdlem22  43677  fourierdlem24  43679  fourierdlem30  43685  fourierdlem37  43692  fourierdlem39  43694  fourierdlem40  43695  fourierdlem41  43696  fourierdlem42  43697  fourierdlem47  43701  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem52  43706  fourierdlem54  43708  fourierdlem60  43714  fourierdlem61  43715  fourierdlem63  43717  fourierdlem64  43718  fourierdlem68  43722  fourierdlem71  43725  fourierdlem72  43726  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem77  43731  fourierdlem78  43732  fourierdlem79  43733  fourierdlem81  43735  fourierdlem82  43736  fourierdlem83  43737  fourierdlem84  43738  fourierdlem87  43741  fourierdlem92  43746  fourierdlem93  43747  fourierdlem94  43748  fourierdlem101  43755  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fourierdlem114  43768  sqwvfoura  43776  sqwvfourb  43777  fouriersw  43779  elaa2lem  43781  etransclem23  43805  etransclem28  43810  etransclem32  43814  etransclem35  43817  etransclem48  43830  qndenserrnbllem  43842  rrnprjdstle  43849  ioorrnopnlem  43852  ioorrnopnxrlem  43854  salexct  43880  sge0fsum  43932  sge0supre  43934  sge0rnbnd  43938  sge0lefi  43943  sge0lessmpt  43944  sge0ltfirp  43945  sge0prle  43946  sge0resrnlem  43948  sge0le  43952  sge0split  43954  sge0iunmptlemre  43960  sge0iunmpt  43963  sge0isum  43972  sge0xaddlem1  43978  sge0xaddlem2  43979  sge0xadd  43980  sge0reuz  43992  sge0reuzb  43993  meaunle  44009  meaiunlelem  44013  voliunsge0lem  44017  meaiuninc  44026  meaiininclem  44031  omeunle  44061  omeiunle  44062  omelesplit  44063  omeiunltfirp  44064  carageniuncllem2  44067  caratheodorylem2  44072  caragencmpl  44080  ovnlecvr  44103  ovncvrrp  44109  ovnsubaddlem1  44115  ovnsubadd  44117  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem5  44144  hoidmvle  44145  ovnhoilem1  44146  ovnlecvr2  44155  ovncvr2  44156  hoiqssbllem2  44168  hspmbllem2  44172  hspmbllem3  44173  ovnsplit  44193  ovolval5lem1  44197  vonioolem1  44225  vonioolem2  44226  vonicclem1  44228  vonicclem2  44229  pimconstlt1  44247  smflimlem2  44317  smflimlem4  44319  smfmullem1  44336  smfsuplem1  44355  smflimsuplem4  44367  smflimsuplem5  44368  iccpartltu  44888  iccpartleu  44891  pgrple2abl  45712  difmodm1lt  45879  nnpw2blen  45937  dignn0flhalflem1  45972  2itscp  46138  upwordnul  46526