Theorem eqbrtrd 4467

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

Syntax hints:   -> wi 4   = wceq 1379   class class class wbr 4447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448

This theorem is referenced by:  eqbrtrrd  4469  somin2  5403  en1b  7580  domunsncan  7614  fodomfi  7795  hartogslem1  7963  wemaplem2  7968  infdifsn  8069  carddomi2  8347  cdaun  8548  cda1dif  8552  mapcdaen  8560  cdaxpdom  8565  cdafi  8566  cdainf  8568  carden  8922  alephsuc3  8951  fpwwe2lem6  9009  fpwwe2lem7  9010  inar1  9149  rankcf  9151  lbinfmle  10494  supmul  10507  rpnnen1lem3  11206  xrmin1  11374  xrmin2  11375  ifle  11392  qbtwnxr  11395  xltnegi  11411  xleadd1a  11441  xlt2add  11448  xlemul1a  11476  xov1plusxeqvd  11662  ubmelm1fzo  11872  flflp1  11908  ceim1l  11938  ceilm1lt  11939  ceille  11941  quoremz  11946  quoremnn0ALT  11948  modlt  11970  modeqmodmin  12020  seqf1olem1  12110  bernneq  12256  discr  12267  faclbnd2  12333  faclbnd4lem3  12337  hashun2  12415  hashfun  12457  ccatsymb  12561  lswccat0lsw  12568  sqrlem6  13040  sqrlem7  13041  rddif  13132  amgm2  13161  climconst  13325  rlimconst  13326  serclim0  13359  rlimcn1  13370  mulcn2  13377  reccn2  13378  o1mul  13396  o1rlimmul  13400  iserex  13438  climlec2  13440  iserge0  13442  climcau  13452  caucvgrlem  13454  caucvgr  13457  iseraltlem2  13464  iseraltlem3  13465  iseralt  13466  fsumabs  13574  o1fsum  13586  iserabs  13588  climfsum  13593  isumless  13616  climcndslem2  13621  divrcnv  13623  flo1  13625  supcvg  13626  georeclim  13640  geomulcvg  13644  cvgrat  13651  mertenslem1  13652  efcvgfsum  13679  eftlub  13701  eflegeo  13713  tanhlt1  13752  tanhbnd  13753  ef01bndlem  13776  sin01bnd  13777  cos01bnd  13778  cos01gt0  13783  ruclem2  13822  ruclem3  13823  ruclem9  13828  ruclem11  13830  ruclem12  13831  bitsfzolem  13939  bitsfzo  13940  bitsinv1lem  13946  sadcaddlem  13962  mulgcd  14039  eucalglt  14069  prmind2  14083  mulgcddvds  14100  isprm5  14108  divdenle  14137  nonsq  14147  pythagtriplem4  14198  pclem  14217  pcpremul  14222  pczdvds  14241  pcprmpw2  14260  qexpz  14275  prmreclem4  14292  prmreclem5  14293  4sqlem10  14320  ramtub  14385  ramub2  14387  natpropd  15199  catciso  15288  p0le  15526  acsdomd  15664  divsgrp  16051  f1otrspeq  16268  pmtrfrn  16279  pmtrfconj  16287  symggen  16291  psgnunilem4  16318  oddvds2  16384  odcau  16420  pgpfi  16421  pgpssslw  16430  sylow3lem4  16446  efgred2  16567  frgp0  16574  odadd2  16648  oddvdssubg  16654  ablfac1c  16912  ablfac1eu  16914  pgpfaclem3  16924  isabvd  17252  abvsubtri  17267  mplsubrg  17873  coe1sfi  18023  cyggic  18378  mp2pm2mplem5  19078  en2top  19253  1stcrest  19720  2ndcrest  19721  hausmapdom  19767  ufilen  20166  xmetrtri2  20594  prdsxmetlem  20606  bl2in  20638  xblcntrps  20648  xblcntr  20649  ssblps  20660  ssbl  20661  blssps  20662  blss  20663  blcld  20743  methaus  20758  metustexhalfOLD  20801  metustexhalf  20802  nrginvrcnlem  20934  nrginvrcn  20935  nmoi  20970  nmo0  20977  nmoid  20984  blcvx  21038  reperflem  21058  reconnlem2  21067  metdcnlem  21076  metdscn  21095  metnrmlem3  21100  mulc1cncf  21144  iccpnfhmeo  21180  cnheiborlem  21189  cnheibor  21190  lebnumii  21201  pcopt  21257  pcopt2  21258  pcoass  21259  nmoleub2lem  21332  nmoleub2lem3  21333  nmoleub2lem2  21334  ipcau2  21412  tchcphlem1  21413  trirn  21562  rrxdstprj1  21571  minveclem3  21579  ivthlem2  21599  ivthlem3  21600  ivth2  21602  ovollb  21625  ovolsslem  21630  ovollb2lem  21634  ovolctb  21636  ovoliunlem1  21648  ovolsca  21661  ovolicc1  21662  ovolicc2lem4  21666  nulmbl  21681  ioombl1lem4  21706  uniioovol  21723  uniioombllem3a  21728  uniioombllem4  21730  opnmbllem  21745  volcn  21750  volivth  21751  i1fadd  21837  i1fmul  21838  mbfi1fseqlem4  21860  mbfi1fseqlem5  21861  mbfi1fseqlem6  21862  itg2const2  21883  itg2seq  21884  itg2uba  21885  itg2split  21891  itg2monolem1  21892  itg2monolem3  21894  itg2i1fseq2  21898  itg2addlem  21900  itg2gt0  21902  itg2cnlem1  21903  itg2cnlem2  21904  itgless  21958  ibladdlem  21961  bddmulibl  21980  dveflem  22115  dvferm1lem  22120  dvferm2lem  22122  dvlip  22129  dvlipcn  22130  dvlip2  22131  dvle  22143  dvivthlem1  22144  lhop1lem  22149  dvcvx  22156  dvfsumabs  22159  dvfsumlem2  22163  dvfsumlem4  22165  dvfsumrlim2  22168  dvfsum2  22170  ftc1a  22173  ftc1lem4  22175  ftc1lem5  22176  deg1sub  22244  ply1divex  22272  deg1submon1p  22288  r1pdeglt  22294  dvdsq1p  22296  fta1glem2  22302  fta1g  22303  plyeq0lem  22342  dgrlt  22397  fta1lem  22437  aalioulem2  22463  aalioulem3  22464  aalioulem4  22465  aaliou3lem2  22473  aaliou3lem9  22480  taylply2  22497  ulmbdd  22527  ulmdvlem1  22529  mtest  22533  mtestbdd  22534  radcnvlem1  22542  radcnvle  22549  pserulm  22551  psercn  22555  pserdvlem2  22557  abelthlem2  22561  abelthlem5  22564  abelthlem7  22567  abelthlem8  22568  abelthlem9  22569  reeff1olem  22575  tangtx  22631  tanord  22658  efif1olem4  22665  logrnaddcl  22690  logcj  22719  logimul  22727  logneg2  22728  logdivlti  22733  divlogrlim  22744  logcnlem3  22753  logcnlem4  22754  efopn  22767  logtayllem  22768  logtayl  22769  cxpcn3lem  22849  cxpaddle  22854  abscxpbnd  22855  asinlem3  22930  asinneg  22945  asinsin  22951  atanlogaddlem  22972  atantan  22982  bndatandm  22988  atans2  22990  atantayl  22996  atantayl2  22997  atantayl3  22998  leibpi  23001  birthdaylem3  23011  rlimcnp  23023  efrlim  23027  cxplim  23029  cxp2lim  23034  cxploglim2  23036  divsqrtsumo1  23041  jensenlem2  23045  amgm  23048  logdifbnd  23051  harmonicbnd4  23068  fsumharmonic  23069  ftalem1  23074  ftalem5  23078  basellem1  23082  basellem8  23089  ppip1le  23163  ppiltx  23179  sqff1o  23184  chtublem  23214  chpub  23223  logfaclbnd  23225  logfacrlim  23227  logexprlim  23228  mersenne  23230  bcmono  23280  bcmax  23281  bposlem2  23288  bposlem5  23291  lgslem3  23301  lgsquadlem1  23357  lgsquadlem2  23358  2sqblem  23380  chebbnd1  23385  chtppilimlem1  23386  chto1ub  23389  chpchtlim  23392  chpo1ubb  23394  rplogsumlem1  23397  rplogsumlem2  23398  rpvmasumlem  23400  dchrisumlem1  23402  dchrisumlem2  23403  dchrmusum2  23407  dchrvmasumlem2  23411  dchrvmasumlem3  23412  dchrvmasumiflem1  23414  dchrisum0flblem1  23421  dchrisum0fno1  23424  dchrisum0lem1b  23428  dchrisum0lem1  23429  dchrisum0lem2a  23430  dchrisum0lem2  23431  rplogsum  23440  mudivsum  23443  mulogsumlem  23444  mulog2sumlem1  23447  mulog2sumlem2  23448  vmalogdivsum2  23451  2vmadivsumlem  23453  selberglem2  23459  selberg2b  23465  logdivbnd  23469  selberg3lem1  23470  selberg3lem2  23471  selberg4lem1  23473  pntrmax  23477  pntrsumo1  23478  pntrlog2bndlem1  23490  pntrlog2bndlem2  23491  pntrlog2bndlem3  23492  pntrlog2bndlem4  23493  pntrlog2bndlem5  23494  pntrlog2bnd  23497  pntpbnd1a  23498  pntpbnd2  23500  pntibndlem2  23504  pntlemb  23510  pntlemg  23511  pntlemh  23512  pntlemr  23515  pntlemj  23516  pntlemf  23518  pntlemo  23520  pnt  23527  padicabv  23543  ostth2lem2  23547  ostth2lem3  23548  ostth3  23551  colperpexlem3  23811  mideulem  23813  brbtwn2  23884  colinearalglem4  23888  nvmtri2  25251  nvabs  25252  nvge0  25253  nvlmle  25278  smcnlem  25283  nmblolbii  25390  blocnilem  25395  siii  25444  ubthlem2  25463  minvecolem3  25468  htthlem  25510  bcsiALT  25772  bcs3  25776  chscllem4  26234  0cnop  26574  0cnfn  26575  nmbdoplbi  26619  nmcoplbi  26623  nmophmi  26626  nmbdfnlbi  26644  nmcfnlbi  26647  nlelchi  26656  riesz1  26660  cnlnadjlem2  26663  nmopadjlei  26683  nmoptrii  26689  nmopcoi  26690  nmopcoadji  26696  unierri  26699  branmfn  26700  pjs14i  26805  hstle  26825  cdj3lem2b  27032  xlt2addrd  27246  eliccelico  27256  elicoelioo  27257  ltesubnnd  27280  archirngz  27395  archiabllem2c  27401  sqsscirc1  27526  tpr2rico  27530  esumcst  27711  measunl  27827  measiun  27829  eulerpartlemgc  27941  eulerpartlemb  27947  ballotlemsel1i  28091  ballotlemro  28101  sgnsub  28123  signsplypnf  28147  signsply0  28148  signsvtn  28181  signsvfnn  28183  lgamgulmlem2  28212  lgamgulmlem3  28213  lgamgulmlem5  28215  lgambdd  28219  lgamcvg2  28237  erdsze2lem1  28287  sinccvglem  28513  divcnvlin  28595  prodfclim1  28604  iprodefisum  28701  faclimlem2  28746  nodense  29026  nobnddown  29038  supadd  29619  ltflcei  29620  opnmbllem0  29627  mblfinlem2  29629  mblfinlem3  29630  ismblfin  29632  itg2addnclem  29643  itg2addnclem2  29644  itg2addnclem3  29645  itg2addnc  29646  ibladdnclem  29648  ftc1cnnclem  29665  ftc1cnnc  29666  ftc1anc  29675  fnemeet1  29787  geomcau  29855  prdsbnd  29892  cntotbnd  29895  heiborlem4  29913  rrndstprj2  29930  rrncmslem  29931  rrnequiv  29934  iccbnd  29939  lzenom  30307  icodiamlt  30360  irrapxlem2  30363  irrapxlem3  30364  irrapxlem5  30366  pellexlem2  30370  pell14qrgt0  30399  pellfundlb  30424  pellfundex  30426  pellfund14  30438  rmspecsqrtnq  30446  jm2.24nn  30501  jm2.17a  30502  jm2.17b  30503  congabseq  30516  acongrep  30522  acongeq  30525  jm2.26lem3  30547  jm2.27a  30551  jm2.27c  30553  hbtlem2  30677  dgraaub  30702  idomodle  30758  lcmledvds  30805  hashnzfzclim  30827  suprnmpt  31029  dstregt0  31040  lefldiveq  31059  absnpncand  31064  fzisoeu  31077  upbdrech  31082  ssfiunibd  31086  ioondisj2  31089  iooabslt  31096  iccshift  31122  iooshift  31126  fmul01  31130  fmul01lt1lem1  31134  fmul01lt1lem2  31135  climrec  31145  climsuse  31150  mullimc  31158  mullimcf  31165  constlimc  31166  idlimc  31168  divcnvg  31169  limcperiod  31170  limcrecl  31171  sumnnodd  31172  lptioo2  31173  lptioo1  31174  islpcn  31181  lptre2pt  31182  limcleqr  31186  neglimc  31189  addlimc  31190  0ellimcdiv  31191  limclner  31193  sinaover2ne0  31204  cncfshift  31212  cncfperiod  31217  cncfioobdlem  31235  cncfioobd  31236  fperdvper  31248  dvdivbd  31253  dvbdfbdioolem1  31258  dvbdfbdioolem2  31259  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  itgiccshift  31298  itgperiod  31299  stoweidlem1  31301  stoweidlem11  31311  stoweidlem13  31313  stoweidlem14  31314  stoweidlem16  31316  stoweidlem21  31321  stoweidlem25  31325  stoweidlem26  31326  stoweidlem36  31336  stoweidlem38  31338  stoweidlem41  31341  stoweidlem42  31342  stoweidlem45  31345  stoweidlem48  31348  stoweidlem52  31352  stoweidlem62  31362  wallispilem3  31367  stirlinglem5  31378  stirlinglem6  31379  stirlinglem7  31380  stirlinglem10  31383  stirlinglem12  31385  stirlinglem15  31388  dirkertrigeqlem1  31398  dirkertrigeqlem3  31400  dirkercncflem1  31403  dirkercncflem4  31406  fourierdlem10  31417  fourierdlem11  31418  fourierdlem12  31419  fourierdlem15  31422  fourierdlem16  31423  fourierdlem19  31426  fourierdlem20  31427  fourierdlem21  31428  fourierdlem22  31429  fourierdlem24  31431  fourierdlem30  31437  fourierdlem37  31444  fourierdlem39  31446  fourierdlem40  31447  fourierdlem41  31448  fourierdlem42  31449  fourierdlem45  31452  fourierdlem47  31454  fourierdlem48  31455  fourierdlem49  31456  fourierdlem50  31457  fourierdlem51  31458  fourierdlem52  31459  fourierdlem54  31461  fourierdlem60  31467  fourierdlem61  31468  fourierdlem62  31469  fourierdlem63  31470  fourierdlem64  31471  fourierdlem65  31472  fourierdlem68  31475  fourierdlem71  31478  fourierdlem72  31479  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem77  31484  fourierdlem78  31485  fourierdlem79  31486  fourierdlem81  31488  fourierdlem83  31490  fourierdlem84  31491  fourierdlem87  31494  fourierdlem92  31499  fourierdlem94  31501  fourierdlem101  31508  fourierdlem102  31509  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  fourierdlem114  31521  sqwvfoura  31529  sqwvfourb  31530  fourierswlem  31531  fouriersw  31532  pgrple2abl  32023  cvlcvr1  34136  cvrat3  34238  dalem25  34494  cdlema1N  34587  dalawlem3  34669  dalawlem4  34670  dalawlem5  34671  dalawlem6  34672  dalawlem7  34673  dalawlem9  34675  dalawlem11  34677  dalawlem12  34678  lhp2lt  34797  lhpmcvr  34819  4atexlemcnd  34868  lautj  34889  trlle  34980  trlval3  34983  trlval4  34984  cdleme0moN  35021  cdleme13  35068  cdleme15  35074  cdleme19b  35100  cdleme20e  35109  cdleme20j  35114  cdleme22e  35140  cdleme22eALTN  35141  cdleme26fALTN  35158  cdleme26f  35159  cdleme27N  35165  cdleme41sn3a  35229  cdleme46fsvlpq  35301  cdlemeg46vrg  35323  cdlemg4  35413  cdlemg7N  35422  cdlemg9a  35428  cdlemg11b  35438  cdlemg12a  35439  trljco  35536  tendoidcl  35565  tendococl  35568  tendopltp  35576  tendo0tp  35585  tendoicl  35592  cdlemi2  35615  cdlemk5a  35631  cdlemk5  35632  cdlemk12  35646  cdlemkole  35649  cdlemk14  35650  cdlemk12u  35668  cdlemk37  35710  cdlemk39s-id  35736  cdlemk49  35747  cdlemk39u1  35763  cdlemk39u  35764  dian0  35836  cdlemm10N  35915  cdlemn2  35992  cdlemn10  36003  dihord1  36015  dihord10  36020  dihmeetlem4preN  36103  dihmeetlem18N  36121  dihmeetlem20N  36123  dihjatc  36214  mapdcnvatN  36463