Theorem eqbrtrd 4441

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

Hypotheses

Ref	Expression
eqbrtrd.1	|- ( ph -> A = B )
eqbrtrd.2	|- ( ph -> B R C )

Assertion

Ref	Expression
eqbrtrd	|- ( ph -> A R C )

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 |- ( ph -> B R C )
2		eqbrtrd.1	. . 3 |- ( ph -> A = B )
3	2	breq1d 4430	. 2 |- ( ph -> ( A R C <-> B R C ) )
4	1, 3	mpbird 235	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1437   class class class wbr 4420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421

This theorem is referenced by:  eqbrtrrd  4443  somin2  5251  en1b  7641  domunsncan  7675  fodomfi  7853  hartogslem1  8060  wemaplem2  8065  infdifsn  8164  carddomi2  8406  cdaun  8603  cda1dif  8607  mapcdaen  8615  cdaxpdom  8620  cdafi  8621  cdainf  8623  carden  8977  alephsuc3  9006  fpwwe2lem6  9061  fpwwe2lem7  9062  inar1  9201  rankcf  9203  lesub3d  10232  lbinfle  10564  lbinfmleOLD  10565  supadd  10576  supmul  10580  rpnnen1lem3  11293  divge1  11368  xrmin1  11473  xrmin2  11474  ifle  11491  qbtwnxr  11494  xltnegi  11510  xleadd1a  11540  xlt2add  11547  xlemul1a  11575  xov1plusxeqvd  11779  ubmelm1fzo  12007  flflp1  12043  ceim1l  12074  ceilm1lt  12075  ceille  12077  quoremz  12082  quoremnn0ALT  12084  modlt  12107  modeqmodmin  12159  seqf1olem1  12252  bernneq  12398  discr  12409  faclbnd2  12476  faclbnd4lem3  12480  hashun2  12562  hashfun  12607  ccatsymb  12720  ccatrn  12726  sqrlem6  13300  sqrlem7  13301  rddif  13392  amgm2  13421  climconst  13595  rlimconst  13596  serclim0  13629  rlimcn1  13640  mulcn2  13647  reccn2  13648  o1mul  13666  o1rlimmul  13670  iserex  13708  climlec2  13710  iserge0  13712  climcau  13722  caucvgrlem  13724  caucvgrlemOLD  13725  caucvgr  13729  iseraltlem2  13737  iseraltlem3  13738  iseralt  13739  fsumabs  13849  o1fsum  13861  iserabs  13863  climfsum  13868  isumless  13891  climcndslem2  13896  divrcnv  13898  flo1  13900  supcvg  13902  georeclim  13916  geomulcvg  13920  cvgrat  13927  mertenslem1  13928  prodfclim1  13937  fprodge1  14037  fprodle  14038  efcvgfsum  14128  eftlub  14151  eflegeo  14163  tanhlt1  14202  tanhbnd  14203  ef01bndlem  14226  sin01bnd  14227  cos01bnd  14228  cos01gt0  14233  ruclem2  14272  ruclem3  14273  ruclem9  14278  ruclem11  14280  ruclem12  14281  bitsfzolem  14395  bitsfzolemOLD  14396  bitsfzo  14397  bitsinv1lem  14403  sadcaddlem  14419  mulgcd  14502  eucalglt  14532  lcmledvds  14552  lcmslefacOLD  14574  lcmfledvds  14593  prmind2  14623  isprm5  14639  mulgcddvds  14649  coprmproddvdslem  14667  divdenle  14686  nonsq  14696  pythagtriplem4  14757  pclem  14776  pcpremul  14781  pczdvds  14800  pcprmpw2  14819  qexpz  14834  prmreclem4  14851  prmreclem5  14852  4sqlem10  14879  ramtub  14956  ramtubOLD  14957  ramub2  14959  prmodvdslcmf  14993  prmorlefacOLD  15006  prmordvdslcmfOLD  15007  prmgaplem8  15016  natpropd  15869  catciso  15990  p0le  16277  acsdomd  16415  qusgrp  16860  f1otrspeq  17076  pmtrfrn  17087  pmtrfconj  17095  symggen  17099  psgnunilem4  17126  oddvds2  17205  odcau  17244  pgpfi  17245  pgpssslw  17254  sylow3lem4  17270  efgred2  17391  frgp0  17398  odadd2  17475  oddvdssubg  17481  ablfac1c  17692  ablfac1eu  17694  pgpfaclem3  17704  isabvd  18036  abvsubtri  18051  mplsubrg  18652  coe1sfi  18794  cyggic  19130  mp2pm2mplem5  19821  en2top  19988  1stcrest  20455  2ndcrest  20456  hausmapdom  20502  ufilen  20932  xmetrtri2  21358  prdsxmetlem  21370  bl2in  21402  xblcntrps  21412  xblcntr  21413  ssblps  21424  ssbl  21425  blssps  21426  blss  21427  blcld  21507  methaus  21522  metustexhalf  21558  nrginvrcnlem  21680  nrginvrcn  21681  nmoi  21720  nmoiOLD  21736  nmo0  21743  nmoid  21750  blcvx  21803  reperflem  21823  reconnlem2  21832  metdcnlem  21841  metdscn  21860  metnrmlem3  21865  metdscnOLD  21875  metnrmlem3OLD  21880  mulc1cncf  21924  iccpnfhmeo  21960  cnheiborlem  21969  cnheibor  21970  lebnumii  21984  pcopt  22040  pcopt2  22041  pcoass  22042  nmoleub2lem  22115  nmoleub2lem3  22116  nmoleub2lem2  22117  ipcau2  22195  tchcphlem1  22196  trirn  22341  rrxdstprj1  22350  minveclem3  22358  minveclem3OLD  22370  ivthlem2  22390  ivthlem3  22391  ivth2  22393  ovollb  22419  ovolsslem  22424  ovollb2lem  22428  ovolctb  22430  ovoliunlem1  22442  ovolsca  22455  ovolicc1  22456  ovolicc2lem4OLD  22460  ovolicc2lem4  22461  nulmbl  22476  ioombl1lem4  22501  uniioovol  22523  uniioombllem3a  22529  uniioombllem4  22531  opnmbllem  22546  volcn  22551  volivth  22552  i1fadd  22640  i1fmul  22641  mbfi1fseqlem4  22663  mbfi1fseqlem5  22664  mbfi1fseqlem6  22665  itg2const2  22686  itg2seq  22687  itg2uba  22688  itg2split  22694  itg2monolem1  22695  itg2monolem3  22697  itg2i1fseq2  22701  itg2addlem  22703  itg2gt0  22705  itg2cnlem1  22706  itg2cnlem2  22707  itgless  22761  ibladdlem  22764  bddmulibl  22783  dveflem  22918  dvferm1lem  22923  dvferm2lem  22925  dvlip  22932  dvlipcn  22933  dvlip2  22934  dvle  22946  dvivthlem1  22947  lhop1lem  22952  dvcvx  22959  dvfsumabs  22962  dvfsumlem2  22966  dvfsumlem4  22968  dvfsumrlim2  22971  dvfsum2  22973  ftc1a  22976  ftc1lem4  22978  ftc1lem5  22979  deg1sub  23044  ply1divex  23074  deg1submon1p  23090  r1pdeglt  23096  dvdsq1p  23098  fta1glem2  23104  fta1g  23105  plyeq0lem  23151  dgrlt  23207  fta1lem  23247  aalioulem2  23276  aalioulem3  23277  aalioulem4  23278  aaliou3lem2  23286  aaliou3lem9  23293  taylply2  23310  ulmbdd  23340  ulmdvlem1  23342  mtest  23346  mtestbdd  23347  radcnvlem1  23355  radcnvle  23362  pserulm  23364  psercn  23368  pserdvlem2  23370  abelthlem2  23374  abelthlem5  23377  abelthlem7  23380  abelthlem8  23381  abelthlem9  23382  reeff1olem  23388  tangtx  23447  tanord  23474  efif1olem4  23481  logrnaddcl  23511  logcj  23542  logimul  23550  logneg2  23551  logdivlti  23556  divlogrlim  23567  logcnlem3  23576  logcnlem4  23577  efopn  23590  logtayllem  23591  logtayl  23592  cxpcn3lem  23674  cxpaddle  23679  abscxpbnd  23680  asinlem3  23784  asinneg  23799  asinsin  23805  atanlogaddlem  23826  atantan  23836  bndatandm  23842  atans2  23844  atantayl  23850  atantayl2  23851  atantayl3  23852  leibpi  23855  birthdaylem3  23866  rlimcnp  23878  efrlim  23882  cxplim  23884  cxp2lim  23889  cxploglim2  23891  divsqrtsumo1  23896  jensenlem2  23900  amgm  23903  logdifbnd  23906  harmonicbnd4  23923  fsumharmonic  23924  lgamgulmlem2  23942  lgamgulmlem3  23943  lgamgulmlem5  23945  lgambdd  23949  lgamcvg2  23967  ftalem1  23984  ftalem5  23988  ftalem5OLD  23990  basellem1  23994  basellem8  24001  ppip1le  24075  ppiltx  24091  sqff1o  24096  chtublem  24126  chpub  24135  logfaclbnd  24137  logfacrlim  24139  logexprlim  24140  mersenne  24142  bcmono  24192  bcmax  24193  bposlem2  24200  bposlem5  24203  lgslem3  24213  lgsquadlem1  24269  lgsquadlem2  24270  2sqblem  24292  chebbnd1  24297  chtppilimlem1  24298  chto1ub  24301  chpchtlim  24304  chpo1ubb  24306  rplogsumlem1  24309  rplogsumlem2  24310  rpvmasumlem  24312  dchrisumlem1  24314  dchrisumlem2  24315  dchrmusum2  24319  dchrvmasumlem2  24323  dchrvmasumlem3  24324  dchrvmasumiflem1  24326  dchrisum0flblem1  24333  dchrisum0fno1  24336  dchrisum0lem1b  24340  dchrisum0lem1  24341  dchrisum0lem2a  24342  dchrisum0lem2  24343  rplogsum  24352  mudivsum  24355  mulogsumlem  24356  mulog2sumlem1  24359  mulog2sumlem2  24360  vmalogdivsum2  24363  2vmadivsumlem  24365  selberglem2  24371  selberg2b  24377  logdivbnd  24381  selberg3lem1  24382  selberg3lem2  24383  selberg4lem1  24385  pntrmax  24389  pntrsumo1  24390  pntrlog2bndlem1  24402  pntrlog2bndlem2  24403  pntrlog2bndlem3  24404  pntrlog2bndlem4  24405  pntrlog2bndlem5  24406  pntrlog2bnd  24409  pntpbnd1a  24410  pntpbnd2  24412  pntibndlem2  24416  pntlemb  24422  pntlemg  24423  pntlemh  24424  pntlemr  24427  pntlemj  24428  pntlemf  24430  pntlemo  24432  pnt  24439  padicabv  24455  ostth2lem2  24459  ostth2lem3  24460  ostth3  24463  colperpexlem3  24761  mideulem2  24763  lnperpex  24832  trgcopy  24833  iscgra1  24839  brbtwn2  24922  colinearalglem4  24926  nvmtri2  26287  nvabs  26288  nvge0  26289  nvlmle  26314  smcnlem  26319  nmblolbii  26426  blocnilem  26431  siii  26480  ubthlem2  26499  minvecolem3  26504  minvecolem3OLD  26514  htthlem  26556  bcsiALT  26818  bcs3  26822  chscllem4  27279  0cnop  27618  0cnfn  27619  nmbdoplbi  27663  nmcoplbi  27667  nmophmi  27670  nmbdfnlbi  27688  nmcfnlbi  27691  nlelchi  27700  riesz1  27704  cnlnadjlem2  27707  nmopadjlei  27727  nmoptrii  27733  nmopcoi  27734  nmopcoadji  27740  unierri  27743  branmfn  27744  pjs14i  27849  hstle  27869  cdj3lem2b  28076  xlt2addrd  28332  eliccelico  28353  elicoelioo  28354  ltesubnnd  28380  archirngz  28501  archiabllem2c  28507  madjusmdetlem2  28650  locfinref  28664  sqsscirc1  28710  tpr2rico  28714  esumcst  28880  esumgect  28907  esum2d  28910  measunl  29034  measiun  29036  omssubaddlem  29123  omssubadd  29124  omssubaddOLD  29128  carsgsigalem  29143  carsgclctunlem2  29147  pmeasmono  29153  eulerpartlemgc  29191  eulerpartlemb  29197  ballotlemsel1i  29341  ballotlemro  29351  ballotlemsel1iOLD  29379  ballotlemroOLD  29389  sgnsub  29411  signsplypnf  29435  signsply0  29436  signsvtn  29469  signsvfnn  29471  erdsze2lem1  29922  sinccvglem  30312  divcnvlin  30362  iprodefisum  30372  faclimlem2  30375  nodense  30571  nobnddown  30583  fnemeet1  31015  ltflcei  31847  ptrecube  31854  poimirlem16  31870  poimirlem17  31871  poimirlem29  31883  broucube  31888  opnmbllem0  31890  mblfinlem2  31892  mblfinlem3  31893  ismblfin  31895  itg2addnclem  31907  itg2addnclem2  31908  itg2addnclem3  31909  itg2addnc  31910  ibladdnclem  31912  ftc1cnnclem  31929  ftc1cnnc  31930  ftc1anc  31939  geomcau  32002  prdsbnd  32039  cntotbnd  32042  heiborlem4  32060  rrndstprj2  32077  rrncmslem  32078  rrnequiv  32081  iccbnd  32086  cvlcvr1  32824  cvrat3  32926  dalem25  33182  cdlema1N  33275  dalawlem3  33357  dalawlem4  33358  dalawlem5  33359  dalawlem6  33360  dalawlem7  33361  dalawlem9  33363  dalawlem11  33365  dalawlem12  33366  lhp2lt  33485  lhpmcvr  33507  4atexlemcnd  33556  lautj  33577  trlle  33669  trlval3  33672  trlval4  33673  cdleme0moN  33710  cdleme13  33757  cdleme15  33763  cdleme19b  33790  cdleme20e  33799  cdleme20j  33804  cdleme22e  33830  cdleme22eALTN  33831  cdleme26fALTN  33848  cdleme26f  33849  cdleme27N  33855  cdleme41sn3a  33919  cdleme46fsvlpq  33991  cdlemeg46vrg  34013  cdlemg4  34103  cdlemg7N  34112  cdlemg9a  34118  cdlemg11b  34128  cdlemg12a  34129  trljco  34226  tendoidcl  34255  tendococl  34258  tendopltp  34266  tendo0tp  34275  tendoicl  34282  cdlemi2  34305  cdlemk5a  34321  cdlemk5  34322  cdlemk12  34336  cdlemkole  34339  cdlemk14  34340  cdlemk12u  34358  cdlemk37  34400  cdlemk39s-id  34426  cdlemk49  34437  cdlemk39u1  34453  cdlemk39u  34454  dian0  34526  cdlemm10N  34605  cdlemn2  34682  cdlemn10  34693  dihord1  34705  dihord10  34710  dihmeetlem4preN  34793  dihmeetlem18N  34811  dihmeetlem20N  34813  dihjatc  34904  mapdcnvatN  35153  lzenom  35531  icodiamlt  35584  irrapxlem2  35587  irrapxlem3  35588  irrapxlem5  35590  pellexlem2  35594  pell14qrgt0  35625  pellfundlb  35652  pellfundex  35654  pellfund14  35666  rmspecsqrtnq  35674  jm2.24nn  35729  jm2.17a  35730  jm2.17b  35731  congabseq  35744  acongrep  35750  acongeq  35753  jm2.26lem3  35776  jm2.27a  35780  jm2.27c  35782  hbtlem2  35903  dgraaub  35933  dgraaubOLD  35934  idomodle  35990  relexpxpmin  36169  frege102d  36206  hashnzfzclim  36529  binomcxplemfrat  36558  binomcxplemnotnn0  36563  suprnmpt  37288  dstregt0  37333  lefldiveq  37348  fzisoeu  37360  upbdrech  37365  ssfiunibd  37369  fzdifsuc2  37372  xadd0ge  37384  supxrgere  37398  supxrge  37403  suplesup  37404  xrlexaddrp  37417  ioondisj2  37420  iccshift  37450  iooshift  37454  fmul01  37478  fmul01lt1lem1  37482  fmul01lt1lem2  37483  climrec  37501  climsuse  37507  mullimc  37516  mullimcf  37523  constlimc  37524  idlimc  37526  divcnvg  37527  limcperiod  37528  limcrecl  37529  lptioo2  37531  lptioo1  37532  islpcn  37539  lptre2pt  37540  limcleqr  37545  neglimc  37548  addlimc  37549  0ellimcdiv  37550  limclner  37552  sinaover2ne0  37563  cncfshift  37571  cncfperiod  37576  cncfioobdlem  37594  cncfioobd  37595  fperdvper  37610  dvdivbd  37615  dvbdfbdioolem1  37620  dvbdfbdioolem2  37621  ioodvbdlimc1lem1  37623  ioodvbdlimc1lem2  37624  ioodvbdlimc1lem1OLD  37625  ioodvbdlimc1lem2OLD  37626  ioodvbdlimc2lem  37628  ioodvbdlimc2lemOLD  37629  dvnmul  37638  dvnprodlem1  37641  itgiccshift  37677  itgperiod  37678  stoweidlem1  37681  stoweidlem11  37691  stoweidlem13  37693  stoweidlem14  37694  stoweidlem16  37696  stoweidlem21  37701  stoweidlem25  37705  stoweidlem26  37706  stoweidlem36  37717  stoweidlem38  37719  stoweidlem41  37722  stoweidlem42  37723  stoweidlem45  37726  stoweidlem48  37729  stoweidlem52  37733  stoweidlem62  37743  stoweidlem62OLD  37744  wallispilem3  37749  stirlinglem5  37760  stirlinglem6  37761  stirlinglem7  37762  stirlinglem10  37765  stirlinglem12  37767  stirlinglem15  37770  dirkercncflem1  37785  fourierdlem10  37799  fourierdlem12  37801  fourierdlem15  37804  fourierdlem16  37805  fourierdlem19  37808  fourierdlem20  37809  fourierdlem21  37810  fourierdlem22  37811  fourierdlem24  37813  fourierdlem30  37819  fourierdlem37  37827  fourierdlem39  37829  fourierdlem40  37830  fourierdlem41  37831  fourierdlem42  37832  fourierdlem42OLD  37833  fourierdlem47  37837  fourierdlem48  37838  fourierdlem49  37839  fourierdlem50  37840  fourierdlem52  37842  fourierdlem54  37844  fourierdlem60  37850  fourierdlem61  37851  fourierdlem63  37853  fourierdlem64  37854  fourierdlem68  37858  fourierdlem71  37861  fourierdlem72  37862  fourierdlem73  37863  fourierdlem74  37864  fourierdlem75  37865  fourierdlem76  37866  fourierdlem77  37867  fourierdlem78  37868  fourierdlem79  37869  fourierdlem81  37871  fourierdlem82  37872  fourierdlem83  37873  fourierdlem84  37874  fourierdlem87  37877  fourierdlem92  37882  fourierdlem93  37883  fourierdlem94  37884  fourierdlem101  37891  fourierdlem102  37892  fourierdlem103  37893  fourierdlem104  37894  fourierdlem111  37901  fourierdlem112  37902  fourierdlem113  37903  fourierdlem114  37904  sqwvfoura  37912  sqwvfourb  37913  fouriersw  37915  elaa2lem  37917  elaa2lemOLD  37918  etransclem23  37942  etransclem28  37947  etransclem32  37951  etransclem35  37954  etransclem48OLD  37967  etransclem48  37968  sge0fsum  38017  sge0supre  38019  sge0rnbnd  38023  sge0lefi  38028  sge0lessmpt  38029  sge0ltfirp  38030  sge0prle  38031  sge0resrnlem  38033  sge0le  38037  sge0split  38039  sge0iunmptlemre  38045  sge0iunmpt  38048  sge0isum  38057  sge0xaddlem1  38063  sge0xaddlem2  38064  sge0xadd  38065  meaunle  38081  meaiunlelem  38085  omeunle  38116  omeiunle  38117  omelesplit  38118  omeiunltfirp  38119  carageniuncllem2  38122  caratheodorylem2  38127  ovnlecvr  38155  ovncvrrp  38161  ovnsubaddlem1  38167  ovnsubadd  38169  iccpartltu  38451  iccpartleu  38454  pgrple2abl  39424  difmodm1lt  39599  nnpw2blen  39665  dignn0flhalflem1  39700