Theorem eqbrtrd 4416

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 4405	. 2 |- ( ph -> ( A R C <-> B R C ) )
4	1, 3	mpbird 240	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1452   class class class wbr 4395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396

This theorem is referenced by:  eqbrtrrd  4418  somin2  5241  en1b  7655  domunsncan  7690  fodomfi  7868  hartogslem1  8075  wemaplem2  8080  infdifsn  8180  carddomi2  8422  cdaun  8620  cda1dif  8624  mapcdaen  8632  cdaxpdom  8637  cdafi  8638  cdainf  8640  carden  8994  alephsuc3  9023  fpwwe2lem6  9078  fpwwe2lem7  9079  inar1  9218  rankcf  9220  lesub3d  10252  lbinfle  10585  lbinfmleOLD  10586  supadd  10597  supmul  10601  rpnnen1lem3  11315  divge1  11390  xrmin1  11495  xrmin2  11496  ifle  11513  qbtwnxr  11516  xltnegi  11532  xleadd1a  11564  xlt2add  11571  xlemul1a  11599  xov1plusxeqvd  11804  ubmelm1fzo  12036  flflp1  12076  ceim1l  12107  ceilm1lt  12108  ceille  12110  quoremz  12115  quoremnn0ALT  12117  modlt  12140  modeqmodmin  12193  addmodlteq  12198  seqf1olem1  12290  bernneq  12436  discr  12447  faclbnd2  12514  faclbnd4lem3  12518  hashun2  12600  hashfun  12650  ccatsymb  12778  ccatrn  12784  sqrlem6  13388  sqrlem7  13389  rddif  13480  amgm2  13509  icodiamlt  13574  climconst  13684  rlimconst  13685  serclim0  13718  rlimcn1  13729  mulcn2  13736  reccn2  13737  o1mul  13755  o1rlimmul  13759  iserex  13797  climlec2  13799  iserge0  13801  climcau  13811  caucvgrlem  13813  caucvgrlemOLD  13814  caucvgr  13818  iseraltlem2  13826  iseraltlem3  13827  iseralt  13828  fsumabs  13938  o1fsum  13950  iserabs  13952  climfsum  13957  isumless  13980  climcndslem2  13985  divrcnv  13987  flo1  13989  supcvg  13991  georeclim  14005  geomulcvg  14009  cvgrat  14016  mertenslem1  14017  prodfclim1  14026  fprodge1  14126  fprodle  14127  efcvgfsum  14217  eftlub  14240  eflegeo  14252  tanhlt1  14291  tanhbnd  14292  ef01bndlem  14315  sin01bnd  14316  cos01bnd  14317  cos01gt0  14322  ruclem2  14361  ruclem3  14362  ruclem9  14367  ruclem11  14369  ruclem12  14370  bitsfzolem  14486  bitsfzolemOLD  14487  bitsfzo  14488  bitsinv1lem  14494  sadcaddlem  14510  mulgcd  14593  eucalglt  14623  lcmledvds  14643  lcmslefacOLD  14665  lcmfledvds  14684  prmind2  14714  isprm5  14730  mulgcddvds  14740  coprmproddvdslem  14758  divdenle  14777  nonsq  14787  pythagtriplem4  14848  pclem  14867  pcpremul  14872  pczdvds  14891  pcprmpw2  14910  qexpz  14925  prmreclem4  14942  prmreclem5  14943  4sqlem10  14970  ramtub  15047  ramtubOLD  15048  ramub2  15050  prmodvdslcmf  15084  prmorlefacOLD  15097  prmordvdslcmfOLD  15098  prmgaplem8  15107  natpropd  15959  catciso  16080  p0le  16367  acsdomd  16505  qusgrp  16950  f1otrspeq  17166  pmtrfrn  17177  pmtrfconj  17185  symggen  17189  psgnunilem4  17216  oddvds2  17295  odcau  17334  pgpfi  17335  pgpssslw  17344  sylow3lem4  17360  efgred2  17481  frgp0  17488  odadd2  17565  oddvdssubg  17571  ablfac1c  17782  ablfac1eu  17784  pgpfaclem3  17794  isabvd  18126  abvsubtri  18141  mplsubrg  18741  coe1sfi  18883  cyggic  19220  mp2pm2mplem5  19911  en2top  20078  1stcrest  20545  2ndcrest  20546  hausmapdom  20592  ufilen  21023  xmetrtri2  21449  prdsxmetlem  21461  bl2in  21493  xblcntrps  21503  xblcntr  21504  ssblps  21515  ssbl  21516  blssps  21517  blss  21518  blcld  21598  methaus  21613  metustexhalf  21649  nrginvrcnlem  21771  nrginvrcn  21772  nmoi  21811  nmoiOLD  21827  nmo0  21834  nmoid  21841  blcvx  21894  reperflem  21914  reconnlem2  21923  metdcnlem  21932  metdscn  21951  metnrmlem3  21956  metdscnOLD  21966  metnrmlem3OLD  21971  mulc1cncf  22015  iccpnfhmeo  22051  cnheiborlem  22060  cnheibor  22061  lebnumii  22075  pcopt  22131  pcopt2  22132  pcoass  22133  nmoleub2lem  22206  nmoleub2lem3  22207  nmoleub2lem2  22208  ipcau2  22286  tchcphlem1  22287  trirn  22432  rrxdstprj1  22441  minveclem3  22449  minveclem3OLD  22461  ivthlem2  22481  ivthlem3  22482  ivth2  22484  ovollb  22510  ovolsslem  22515  ovollb2lem  22519  ovolctb  22521  ovoliunlem1  22533  ovolsca  22546  ovolicc1  22547  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  nulmbl  22567  ioombl1lem4  22593  uniioovol  22615  uniioombllem3a  22621  uniioombllem4  22623  opnmbllem  22638  volcn  22643  volivth  22644  i1fadd  22732  i1fmul  22733  mbfi1fseqlem4  22755  mbfi1fseqlem5  22756  mbfi1fseqlem6  22757  itg2const2  22778  itg2seq  22779  itg2uba  22780  itg2split  22786  itg2monolem1  22787  itg2monolem3  22789  itg2i1fseq2  22793  itg2addlem  22795  itg2gt0  22797  itg2cnlem1  22798  itg2cnlem2  22799  itgless  22853  ibladdlem  22856  bddmulibl  22875  dveflem  23010  dvferm1lem  23015  dvferm2lem  23017  dvlip  23024  dvlipcn  23025  dvlip2  23026  dvle  23038  dvivthlem1  23039  lhop1lem  23044  dvcvx  23051  dvfsumabs  23054  dvfsumlem2  23058  dvfsumlem4  23060  dvfsumrlim2  23063  dvfsum2  23065  ftc1a  23068  ftc1lem4  23070  ftc1lem5  23071  deg1sub  23136  ply1divex  23166  deg1submon1p  23182  r1pdeglt  23188  dvdsq1p  23190  fta1glem2  23196  fta1g  23197  plyeq0lem  23243  dgrlt  23299  fta1lem  23339  aalioulem2  23368  aalioulem3  23369  aalioulem4  23370  aaliou3lem2  23378  aaliou3lem9  23385  taylply2  23402  ulmbdd  23432  ulmdvlem1  23434  mtest  23438  mtestbdd  23439  radcnvlem1  23447  radcnvle  23454  pserulm  23456  psercn  23460  pserdvlem2  23462  abelthlem2  23466  abelthlem5  23469  abelthlem7  23472  abelthlem8  23473  abelthlem9  23474  reeff1olem  23480  tangtx  23539  tanord  23566  efif1olem4  23573  logrnaddcl  23603  logcj  23634  logimul  23642  logneg2  23643  logdivlti  23648  divlogrlim  23659  logcnlem3  23668  logcnlem4  23669  efopn  23682  logtayllem  23683  logtayl  23684  cxpcn3lem  23766  cxpaddle  23771  abscxpbnd  23772  asinlem3  23876  asinneg  23891  asinsin  23897  atanlogaddlem  23918  atantan  23928  bndatandm  23934  atans2  23936  atantayl  23942  atantayl2  23943  atantayl3  23944  leibpi  23947  birthdaylem3  23958  rlimcnp  23970  efrlim  23974  cxplim  23976  cxp2lim  23981  cxploglim2  23983  divsqrtsumo1  23988  jensenlem2  23992  amgm  23995  logdifbnd  23998  harmonicbnd4  24015  fsumharmonic  24016  lgamgulmlem2  24034  lgamgulmlem3  24035  lgamgulmlem5  24037  lgambdd  24041  lgamcvg2  24059  ftalem1  24076  ftalem5  24080  ftalem5OLD  24082  basellem1  24086  basellem8  24093  ppip1le  24167  ppiltx  24183  sqff1o  24188  chtublem  24218  chpub  24227  logfaclbnd  24229  logfacrlim  24231  logexprlim  24232  mersenne  24234  bcmono  24284  bcmax  24285  bposlem2  24292  bposlem5  24295  lgslem3  24305  lgsquadlem1  24361  lgsquadlem2  24362  2sqblem  24384  chebbnd1  24389  chtppilimlem1  24390  chto1ub  24393  chpchtlim  24396  chpo1ubb  24398  rplogsumlem1  24401  rplogsumlem2  24402  rpvmasumlem  24404  dchrisumlem1  24406  dchrisumlem2  24407  dchrmusum2  24411  dchrvmasumlem2  24415  dchrvmasumlem3  24416  dchrvmasumiflem1  24418  dchrisum0flblem1  24425  dchrisum0fno1  24428  dchrisum0lem1b  24432  dchrisum0lem1  24433  dchrisum0lem2a  24434  dchrisum0lem2  24435  rplogsum  24444  mudivsum  24447  mulogsumlem  24448  mulog2sumlem1  24451  mulog2sumlem2  24452  vmalogdivsum2  24455  2vmadivsumlem  24457  selberglem2  24463  selberg2b  24469  logdivbnd  24473  selberg3lem1  24474  selberg3lem2  24475  selberg4lem1  24477  pntrmax  24481  pntrsumo1  24482  pntrlog2bndlem1  24494  pntrlog2bndlem2  24495  pntrlog2bndlem3  24496  pntrlog2bndlem4  24497  pntrlog2bndlem5  24498  pntrlog2bnd  24501  pntpbnd1a  24502  pntpbnd2  24504  pntibndlem2  24508  pntlemb  24514  pntlemg  24515  pntlemh  24516  pntlemr  24519  pntlemj  24520  pntlemf  24522  pntlemo  24524  pnt  24531  padicabv  24547  ostth2lem2  24551  ostth2lem3  24552  ostth3  24555  colperpexlem3  24853  mideulem2  24855  lnperpex  24924  trgcopy  24925  iscgra1  24931  brbtwn2  25014  colinearalglem4  25018  nvmtri2  26382  nvabs  26383  nvge0  26384  nvlmle  26409  smcnlem  26414  nmblolbii  26521  blocnilem  26526  siii  26575  ubthlem2  26594  minvecolem3  26599  minvecolem3OLD  26609  htthlem  26651  bcsiALT  26913  bcs3  26917  chscllem4  27374  0cnop  27713  0cnfn  27714  nmbdoplbi  27758  nmcoplbi  27762  nmophmi  27765  nmbdfnlbi  27783  nmcfnlbi  27786  nlelchi  27795  riesz1  27799  cnlnadjlem2  27802  nmopadjlei  27822  nmoptrii  27828  nmopcoi  27829  nmopcoadji  27835  unierri  27838  branmfn  27839  pjs14i  27944  hstle  27964  cdj3lem2b  28171  xlt2addrd  28413  eliccelico  28434  elicoelioo  28435  ltesubnnd  28460  archirngz  28580  archiabllem2c  28586  madjusmdetlem2  28728  locfinref  28742  sqsscirc1  28788  tpr2rico  28792  esumcst  28958  esumgect  28985  esum2d  28988  measunl  29112  measiun  29114  omssubaddlem  29200  omssubadd  29201  omssubaddOLD  29205  carsgsigalem  29220  carsgclctunlem2  29224  pmeasmono  29230  eulerpartlemgc  29268  eulerpartlemb  29274  ballotlemsel1i  29418  ballotlemro  29428  ballotlemsel1iOLD  29456  ballotlemroOLD  29466  sgnsub  29488  signsplypnf  29511  signsply0  29512  signsvtn  29545  signsvfnn  29547  erdsze2lem1  29998  sinccvglem  30388  divcnvlin  30438  iprodefisum  30448  faclimlem2  30451  nodense  30649  nobnddown  30661  fnemeet1  31093  ltflcei  31997  ptrecube  32004  poimirlem16  32020  poimirlem17  32021  poimirlem29  32033  broucube  32038  opnmbllem0  32040  mblfinlem2  32042  mblfinlem3  32043  ismblfin  32045  itg2addnclem  32057  itg2addnclem2  32058  itg2addnclem3  32059  itg2addnc  32060  ibladdnclem  32062  ftc1cnnclem  32079  ftc1cnnc  32080  ftc1anc  32089  geomcau  32152  prdsbnd  32189  cntotbnd  32192  heiborlem4  32210  rrndstprj2  32227  rrncmslem  32228  rrnequiv  32231  iccbnd  32236  cvlcvr1  32976  cvrat3  33078  dalem25  33334  cdlema1N  33427  dalawlem3  33509  dalawlem4  33510  dalawlem5  33511  dalawlem6  33512  dalawlem7  33513  dalawlem9  33515  dalawlem11  33517  dalawlem12  33518  lhp2lt  33637  lhpmcvr  33659  4atexlemcnd  33708  lautj  33729  trlle  33821  trlval3  33824  trlval4  33825  cdleme0moN  33862  cdleme13  33909  cdleme15  33915  cdleme19b  33942  cdleme20e  33951  cdleme20j  33956  cdleme22e  33982  cdleme22eALTN  33983  cdleme26fALTN  34000  cdleme26f  34001  cdleme27N  34007  cdleme41sn3a  34071  cdleme46fsvlpq  34143  cdlemeg46vrg  34165  cdlemg4  34255  cdlemg7N  34264  cdlemg9a  34270  cdlemg11b  34280  cdlemg12a  34281  trljco  34378  tendoidcl  34407  tendococl  34410  tendopltp  34418  tendo0tp  34427  tendoicl  34434  cdlemi2  34457  cdlemk5a  34473  cdlemk5  34474  cdlemk12  34488  cdlemkole  34491  cdlemk14  34492  cdlemk12u  34510  cdlemk37  34552  cdlemk39s-id  34578  cdlemk49  34589  cdlemk39u1  34605  cdlemk39u  34606  dian0  34678  cdlemm10N  34757  cdlemn2  34834  cdlemn10  34845  dihord1  34857  dihord10  34862  dihmeetlem4preN  34945  dihmeetlem18N  34963  dihmeetlem20N  34965  dihjatc  35056  mapdcnvatN  35305  lzenom  35683  irrapxlem2  35738  irrapxlem3  35739  irrapxlem5  35741  pellexlem2  35745  pell14qrgt0  35776  pellfundlb  35803  pellfundex  35805  pellfund14  35817  rmspecsqrtnq  35825  jm2.24nn  35880  jm2.17a  35881  jm2.17b  35882  congabseq  35895  acongrep  35901  acongeq  35904  jm2.26lem3  35927  jm2.27a  35931  jm2.27c  35933  hbtlem2  36054  dgraaub  36084  dgraaubOLD  36085  idomodle  36141  relexpxpmin  36380  frege102d  36417  hashnzfzclim  36741  binomcxplemfrat  36770  binomcxplemnotnn0  36775  suprnmpt  37512  mpct  37553  dstregt0  37581  lefldiveq  37595  fzisoeu  37606  upbdrech  37611  ssfiunibd  37615  fzdifsuc2  37618  xadd0ge  37630  supxrgere  37643  supxrge  37648  suplesup  37649  xrlexaddrp  37662  infxrunb2  37678  infleinflem2  37681  ioondisj2  37685  iccshift  37715  iooshift  37719  fmul01  37755  fmul01lt1lem1  37759  fmul01lt1lem2  37760  climrec  37778  climsuse  37784  mullimc  37793  mullimcf  37800  constlimc  37801  idlimc  37803  divcnvg  37804  limcperiod  37805  limcrecl  37806  lptioo2  37808  lptioo1  37809  islpcn  37816  lptre2pt  37817  limcleqr  37822  neglimc  37825  addlimc  37826  0ellimcdiv  37827  limclner  37829  sinaover2ne0  37840  cncfshift  37848  cncfperiod  37853  cncfioobdlem  37871  cncfioobd  37872  fperdvper  37887  dvdivbd  37892  dvbdfbdioolem1  37897  dvbdfbdioolem2  37898  ioodvbdlimc1lem1  37900  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem1OLD  37902  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvnmul  37915  dvnprodlem1  37918  itgiccshift  37954  itgperiod  37955  ismbl3  37961  ovolsplit  37963  stoweidlem1  37973  stoweidlem11  37983  stoweidlem13  37985  stoweidlem14  37986  stoweidlem16  37988  stoweidlem21  37993  stoweidlem25  37997  stoweidlem26  37998  stoweidlem36  38009  stoweidlem38  38011  stoweidlem41  38014  stoweidlem42  38015  stoweidlem45  38018  stoweidlem48  38021  stoweidlem52  38025  stoweidlem62  38035  stoweidlem62OLD  38036  wallispilem3  38041  stirlinglem5  38052  stirlinglem6  38053  stirlinglem7  38054  stirlinglem10  38057  stirlinglem12  38059  stirlinglem15  38062  dirkercncflem1  38077  fourierdlem10  38091  fourierdlem12  38093  fourierdlem15  38096  fourierdlem16  38097  fourierdlem19  38100  fourierdlem20  38101  fourierdlem21  38102  fourierdlem22  38103  fourierdlem24  38105  fourierdlem30  38111  fourierdlem37  38119  fourierdlem39  38121  fourierdlem40  38122  fourierdlem41  38123  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem47  38129  fourierdlem48  38130  fourierdlem49  38131  fourierdlem50  38132  fourierdlem52  38134  fourierdlem54  38136  fourierdlem60  38142  fourierdlem61  38143  fourierdlem63  38145  fourierdlem64  38146  fourierdlem68  38150  fourierdlem71  38153  fourierdlem72  38154  fourierdlem73  38155  fourierdlem74  38156  fourierdlem75  38157  fourierdlem76  38158  fourierdlem77  38159  fourierdlem78  38160  fourierdlem79  38161  fourierdlem81  38163  fourierdlem82  38164  fourierdlem83  38165  fourierdlem84  38166  fourierdlem87  38169  fourierdlem92  38174  fourierdlem93  38175  fourierdlem94  38176  fourierdlem101  38183  fourierdlem102  38184  fourierdlem103  38185  fourierdlem104  38186  fourierdlem111  38193  fourierdlem112  38194  fourierdlem113  38195  fourierdlem114  38196  sqwvfoura  38204  sqwvfourb  38205  fouriersw  38207  elaa2lem  38209  elaa2lemOLD  38210  etransclem23  38234  etransclem28  38239  etransclem32  38243  etransclem35  38246  etransclem48OLD  38259  etransclem48  38260  qndenserrnbllem  38275  salexct  38305  sge0fsum  38343  sge0supre  38345  sge0rnbnd  38349  sge0lefi  38354  sge0lessmpt  38355  sge0ltfirp  38356  sge0prle  38357  sge0resrnlem  38359  sge0le  38363  sge0split  38365  sge0iunmptlemre  38371  sge0iunmpt  38374  sge0isum  38383  sge0xaddlem1  38389  sge0xaddlem2  38390  sge0xadd  38391  meaunle  38418  meaiunlelem  38422  voliunsge0lem  38426  omeunle  38456  omeiunle  38457  omelesplit  38458  omeiunltfirp  38459  carageniuncllem2  38462  caratheodorylem2  38467  caragencmpl  38475  ovnlecvr  38498  ovncvrrp  38504  ovnsubaddlem1  38510  ovnsubadd  38512  hoidmv1lelem1  38531  hoidmv1lelem2  38532  hoidmv1le  38534  hoidmvlelem1  38535  hoidmvlelem2  38536  hoidmvlelem5  38539  hoidmvle  38540  ovnhoilem1  38541  ovnlecvr2  38550  ovncvr2  38551  hoiqssbllem2  38563  hspmbllem2  38567  hspmbllem3  38568  ovnsplit  38588  ovolval5lem1  38592  iccpartltu  38884  iccpartleu  38887  subupgr  39523  crctcsh1wlkn0lem1  39988  pgrple2abl  40658  difmodm1lt  40833  nnpw2blen  40899  dignn0flhalflem1  40934