Theorem eqbrtrd 4675

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

Syntax hints:   -> wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  eqbrtrrd  4677  somin2  5531  en1b  8024  domunsncan  8060  fodomfi  8239  hartogslem1  8447  wemaplem2  8452  infdifsn  8554  carddomi2  8796  cdaun  8994  cda1dif  8998  mapcdaen  9006  cdaxpdom  9011  cdafi  9012  cdainf  9014  carden  9373  alephsuc3  9402  fpwwe2lem6  9457  fpwwe2lem7  9458  inar1  9597  rankcf  9599  lesub3d  10645  lbinfle  10978  supadd  10991  supmul  10995  rpnnen1lem3  11816  rpnnen1lem3OLD  11822  divge1  11898  xrmin1  12008  xrmin2  12009  ifle  12028  qbtwnxr  12031  xltnegi  12047  xleadd1a  12083  xlt2add  12090  xlemul1a  12118  xov1plusxeqvd  12318  ubmelm1fzo  12564  flflp1  12608  ceim1l  12646  ceilm1lt  12647  ceille  12649  quoremz  12654  quoremnn0ALT  12656  modlt  12679  modeqmodmin  12740  addmodlteq  12745  seqf1olem1  12840  bernneq  12990  discr  13001  faclbnd2  13078  faclbnd4lem3  13082  hashun2  13172  hashfun  13224  ccatsymb  13366  ccatrn  13372  sqrlem6  13988  sqrlem7  13989  rddif  14080  amgm2  14109  icodiamlt  14174  climconst  14274  rlimconst  14275  serclim0  14308  rlimcn1  14319  mulcn2  14326  reccn2  14327  o1mul  14345  o1rlimmul  14349  iserex  14387  climlec2  14389  iserge0  14391  climcau  14401  caucvgrlem  14403  caucvgr  14406  iseraltlem2  14413  iseraltlem3  14414  iseralt  14415  fsumabs  14533  o1fsum  14545  iserabs  14547  climfsum  14552  isumless  14577  climcndslem2  14582  divrcnv  14584  flo1  14586  supcvg  14588  georeclim  14603  geomulcvg  14607  cvgrat  14615  mertenslem1  14616  prodfclim1  14625  fprodge1  14726  fprodle  14727  efcvgfsum  14816  eftlub  14839  eflegeo  14851  tanhlt1  14890  tanhbnd  14891  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  cos01gt0  14921  ruclem2  14961  ruclem3  14962  ruclem9  14967  ruclem11  14969  ruclem12  14970  bitsfzolem  15156  bitsfzo  15157  bitsinv1lem  15163  sadcaddlem  15179  mulgcd  15265  eucalglt  15298  lcmledvds  15312  lcmfledvds  15345  mulgcddvds  15369  coprmproddvdslem  15376  prmind2  15398  isprm5  15419  divdenle  15457  nonsq  15467  pythagtriplem4  15524  pclem  15543  pcpremul  15548  pczdvds  15567  pcprmpw2  15586  qexpz  15605  prmreclem4  15623  prmreclem5  15624  4sqlem10  15651  ramtub  15716  ramub2  15718  prmodvdslcmf  15751  prmgaplem8  15762  natpropd  16636  catciso  16757  p0le  17043  acsdomd  17181  qusgrp  17649  f1otrspeq  17867  pmtrfrn  17878  pmtrfconj  17886  symggen  17890  psgnunilem4  17917  oddvds2  17983  odcau  18019  pgpfi  18020  pgpssslw  18029  sylow3lem4  18045  efgred2  18166  frgp0  18173  odadd2  18252  oddvdssubg  18258  ablfac1c  18470  ablfac1eu  18472  pgpfaclem3  18482  isabvd  18820  abvsubtri  18835  mplsubrg  19440  coe1sfi  19583  cyggic  19921  mp2pm2mplem5  20615  en2top  20789  1stcrest  21256  2ndcrest  21257  hausmapdom  21303  ufilen  21734  xmetrtri2  22161  prdsxmetlem  22173  bl2in  22205  xblcntrps  22215  xblcntr  22216  ssblps  22227  ssbl  22228  blssps  22229  blss  22230  blcld  22310  methaus  22325  metustexhalf  22361  nmtri2  22431  tngngp3  22460  nrginvrcnlem  22495  nrginvrcn  22496  nmoi  22532  nmo0  22539  nmoid  22546  blcvx  22601  reperflem  22621  reconnlem2  22630  metdcnlem  22639  metdscn  22659  metnrmlem3  22664  mulc1cncf  22708  iccpnfhmeo  22744  cnheiborlem  22753  cnheibor  22754  lebnumii  22765  pcopt  22822  pcopt2  22823  pcoass  22824  nmoleub2lem  22914  nmoleub2lem3  22915  nmoleub2lem2  22916  ipcau2  23033  tchcphlem1  23034  nglmle  23100  trirn  23183  rrxdstprj1  23192  minveclem3  23200  ivthlem2  23221  ivthlem3  23222  ivth2  23224  ovollb  23247  ovolsslem  23252  ovollb2lem  23256  ovolctb  23258  ovoliunlem1  23270  ovolsca  23283  ovolicc1  23284  ovolicc2lem4  23288  nulmbl  23303  ioombl1lem4  23329  uniioovol  23347  uniioombllem3a  23352  uniioombllem4  23354  opnmbllem  23369  volcn  23374  volivth  23375  i1fadd  23462  i1fmul  23463  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  itg2const2  23508  itg2seq  23509  itg2uba  23510  itg2split  23516  itg2monolem1  23517  itg2monolem3  23519  itg2i1fseq2  23523  itg2addlem  23525  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  itgless  23583  ibladdlem  23586  bddmulibl  23605  dveflem  23742  dvferm1lem  23747  dvferm2lem  23749  dvlip  23756  dvlipcn  23757  dvlip2  23758  dvle  23770  dvivthlem1  23771  lhop1lem  23776  dvcvx  23783  dvfsumabs  23786  dvfsumlem2  23790  dvfsumlem4  23792  dvfsumrlim2  23795  dvfsum2  23797  ftc1a  23800  ftc1lem4  23802  ftc1lem5  23803  deg1sub  23868  ply1divex  23896  deg1submon1p  23912  r1pdeglt  23918  dvdsq1p  23920  fta1glem2  23926  fta1g  23927  plyeq0lem  23966  dgrlt  24022  fta1lem  24062  aalioulem2  24088  aalioulem3  24089  aalioulem4  24090  aaliou3lem2  24098  aaliou3lem9  24105  taylply2  24122  ulmbdd  24152  ulmdvlem1  24154  mtest  24158  mtestbdd  24159  radcnvlem1  24167  radcnvle  24174  pserulm  24176  psercn  24180  pserdvlem2  24182  abelthlem2  24186  abelthlem5  24189  abelthlem7  24192  abelthlem8  24193  abelthlem9  24194  reeff1olem  24200  tangtx  24257  tanord  24284  efif1olem4  24291  logrnaddcl  24321  logcj  24352  logimul  24360  logneg2  24361  logdivlti  24366  divlogrlim  24381  logcnlem3  24390  logcnlem4  24391  efopn  24404  logtayllem  24405  logtayl  24406  cxpcn3lem  24488  cxpaddle  24493  abscxpbnd  24494  asinlem3  24598  asinneg  24613  asinsin  24619  atanlogaddlem  24640  atantan  24650  bndatandm  24656  atans2  24658  atantayl  24664  atantayl2  24665  atantayl3  24666  leibpi  24669  birthdaylem3  24680  rlimcnp  24692  efrlim  24696  cxplim  24698  cxp2lim  24703  cxploglim2  24705  divsqrtsumo1  24710  jensenlem2  24714  amgm  24717  logdifbnd  24720  harmonicbnd4  24737  fsumharmonic  24738  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem5  24759  lgambdd  24763  lgamcvg2  24781  ftalem1  24799  ftalem5  24803  basellem1  24807  basellem8  24814  ppip1le  24887  ppiltx  24903  sqff1o  24908  chtublem  24936  chpub  24945  logfaclbnd  24947  logfacrlim  24949  logexprlim  24950  mersenne  24952  bcmono  25002  bcmax  25003  bposlem2  25010  bposlem5  25013  lgslem3  25024  gausslemma2dlem1a  25090  lgsquadlem1  25105  lgsquadlem2  25106  2lgslem1c  25118  2sqblem  25156  chebbnd1  25161  chtppilimlem1  25162  chto1ub  25165  chpchtlim  25168  chpo1ubb  25170  rplogsumlem1  25173  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlem1  25178  dchrisumlem2  25179  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  dchrisum0fno1  25200  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  rplogsum  25216  mudivsum  25219  mulogsumlem  25220  mulog2sumlem1  25223  mulog2sumlem2  25224  vmalogdivsum2  25227  2vmadivsumlem  25229  selberglem2  25235  selberg2b  25241  logdivbnd  25245  selberg3lem1  25246  selberg3lem2  25247  selberg4lem1  25249  pntrmax  25253  pntrsumo1  25254  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem2  25280  pntlemb  25286  pntlemg  25287  pntlemh  25288  pntlemr  25291  pntlemj  25292  pntlemf  25294  pntlemo  25296  pnt  25303  padicabv  25319  ostth2lem2  25323  ostth2lem3  25324  ostth3  25327  colperpexlem3  25624  mideulem2  25626  lnperpex  25695  trgcopy  25696  iscgra1  25702  brbtwn2  25785  colinearalglem4  25789  subupgr  26179  crctcshwlkn0lem1  26702  nvabs  27527  nvge0  27528  smcnlem  27552  nmblolbii  27654  blocnilem  27659  siii  27708  ubthlem2  27727  minvecolem3  27732  htthlem  27774  bcsiALT  28036  bcs3  28040  chscllem4  28499  0cnop  28838  0cnfn  28839  nmbdoplbi  28883  nmcoplbi  28887  nmophmi  28890  nmbdfnlbi  28908  nmcfnlbi  28911  nlelchi  28920  riesz1  28924  cnlnadjlem2  28927  nmopadjlei  28947  nmoptrii  28953  nmopcoi  28954  nmopcoadji  28960  unierri  28963  branmfn  28964  pjs14i  29069  hstle  29089  cdj3lem2b  29296  xlt2addrd  29523  eliccelico  29539  elicoelioo  29540  ltesubnnd  29568  archirngz  29743  archiabllem2c  29749  madjusmdetlem2  29894  locfinref  29908  sqsscirc1  29954  tpr2rico  29958  esumcst  30125  esumgect  30152  esum2d  30155  measunl  30279  measiun  30281  omssubaddlem  30361  omssubadd  30362  carsgsigalem  30377  carsgclctunlem2  30381  pmeasmono  30386  eulerpartlemgc  30424  eulerpartlemb  30430  ballotlemsel1i  30574  ballotlemro  30584  sgnsub  30606  signsplypnf  30627  signsply0  30628  signsvtn  30661  signsvfnn  30663  hgt750lemd  30726  logdivsqrle  30728  erdsze2lem1  31185  sinccvglem  31566  divcnvlin  31618  iprodefisum  31627  faclimlem2  31630  nosep1o  31832  nodense  31842  fnemeet1  32361  dnibndlem10  32477  dnibndlem11  32478  dnibnd  32481  knoppcnlem4  32486  knoppcnlem6  32488  unblimceq0lem  32497  unblimceq0  32498  unbdqndv2lem1  32500  unbdqndv2lem2  32501  knoppndvlem11  32513  knoppndvlem12  32514  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem18  32520  knoppndvlem19  32521  knoppndvlem21  32523  ltflcei  33397  ptrecube  33409  poimirlem16  33425  poimirlem17  33426  poimirlem29  33438  broucube  33443  opnmbllem0  33445  mblfinlem2  33447  mblfinlem3  33448  ismblfin  33450  itg2addnclem  33461  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  ibladdnclem  33466  ftc1cnnclem  33483  ftc1cnnc  33484  ftc1anc  33493  geomcau  33555  prdsbnd  33592  cntotbnd  33595  heiborlem4  33613  rrndstprj2  33630  rrncmslem  33631  rrnequiv  33634  iccbnd  33639  cvlcvr1  34626  cvrat3  34728  dalem25  34984  cdlema1N  35077  dalawlem3  35159  dalawlem4  35160  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  lhp2lt  35287  lhpmcvr  35309  4atexlemcnd  35358  lautj  35379  trlle  35471  trlval3  35474  trlval4  35475  cdleme0moN  35512  cdleme13  35559  cdleme15  35565  cdleme19b  35592  cdleme20e  35601  cdleme20j  35606  cdleme22e  35632  cdleme22eALTN  35633  cdleme26fALTN  35650  cdleme26f  35651  cdleme27N  35657  cdleme41sn3a  35721  cdleme46fsvlpq  35793  cdlemeg46vrg  35815  cdlemg4  35905  cdlemg7N  35914  cdlemg9a  35920  cdlemg11b  35930  cdlemg12a  35931  trljco  36028  tendoidcl  36057  tendococl  36060  tendopltp  36068  tendo0tp  36077  tendoicl  36084  cdlemi2  36107  cdlemk5a  36123  cdlemk5  36124  cdlemk12  36138  cdlemkole  36141  cdlemk14  36142  cdlemk12u  36160  cdlemk37  36202  cdlemk39s-id  36228  cdlemk49  36239  cdlemk39u1  36255  cdlemk39u  36256  dian0  36328  cdlemm10N  36407  cdlemn2  36484  cdlemn10  36495  dihord1  36507  dihord10  36512  dihmeetlem4preN  36595  dihmeetlem18N  36613  dihmeetlem20N  36615  dihjatc  36706  mapdcnvatN  36955  lzenom  37333  irrapxlem2  37387  irrapxlem3  37388  irrapxlem5  37390  pellexlem2  37394  pell14qrgt0  37423  pellfundlb  37448  pellfundex  37450  pellfund14  37462  rmspecsqrtnq  37470  rmspecsqrtnqOLD  37471  jm2.24nn  37526  jm2.17a  37527  jm2.17b  37528  congabseq  37541  acongrep  37547  acongeq  37550  jm2.26lem3  37568  jm2.27a  37572  jm2.27c  37574  hbtlem2  37694  dgraaub  37718  idomodle  37774  relexpxpmin  38009  frege102d  38046  hashnzfzclim  38521  binomcxplemfrat  38550  binomcxplemnotnn0  38555  suprnmpt  39355  mpct  39393  rnmptbddlem  39455  dstregt0  39493  lefldiveq  39505  fzisoeu  39514  upbdrech  39519  ssfiunibd  39523  fzdifsuc2  39525  xadd0ge  39536  supxrgere  39549  supxrge  39554  suplesup  39555  xrlexaddrp  39568  infxrunb2  39584  infleinflem2  39587  reclt0d  39607  infrpgernmpt  39695  ioondisj2  39714  iccshift  39744  iooshift  39748  fmul01  39812  fmul01lt1lem1  39816  fmul01lt1lem2  39817  climrec  39835  climsuse  39840  mullimc  39848  mullimcf  39855  constlimc  39856  idlimc  39858  divcnvg  39859  limcperiod  39860  limcrecl  39861  lptioo2  39863  lptioo1  39864  islpcn  39871  lptre2pt  39872  limcleqr  39876  neglimc  39879  addlimc  39880  0ellimcdiv  39881  limclner  39883  climleltrp  39908  limsuplesup  39931  limsupmnflem  39952  supcnvlimsupmpt  39973  0cnv  39974  xlimconst  40051  sinaover2ne0  40079  cncfshift  40087  cncfperiod  40092  cncfioobdlem  40109  cncfioobd  40110  fperdvper  40133  dvdivbd  40138  dvbdfbdioolem1  40143  dvbdfbdioolem2  40144  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnmul  40158  dvnprodlem1  40161  itgiccshift  40196  itgperiod  40197  ismbl3  40203  ovolsplit  40205  stoweidlem1  40218  stoweidlem11  40228  stoweidlem13  40230  stoweidlem14  40231  stoweidlem16  40233  stoweidlem21  40238  stoweidlem25  40242  stoweidlem26  40243  stoweidlem36  40253  stoweidlem38  40255  stoweidlem41  40258  stoweidlem42  40259  stoweidlem45  40262  stoweidlem48  40265  stoweidlem52  40269  stoweidlem62  40279  wallispilem3  40284  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  stirlinglem12  40302  stirlinglem15  40305  dirkercncflem1  40320  fourierdlem10  40334  fourierdlem12  40336  fourierdlem15  40339  fourierdlem16  40340  fourierdlem19  40343  fourierdlem20  40344  fourierdlem21  40345  fourierdlem22  40346  fourierdlem24  40348  fourierdlem30  40354  fourierdlem37  40361  fourierdlem39  40363  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem47  40370  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem52  40375  fourierdlem54  40377  fourierdlem60  40383  fourierdlem61  40384  fourierdlem63  40386  fourierdlem64  40387  fourierdlem68  40391  fourierdlem71  40394  fourierdlem72  40395  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem77  40400  fourierdlem78  40401  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem83  40406  fourierdlem84  40407  fourierdlem87  40410  fourierdlem92  40415  fourierdlem93  40416  fourierdlem94  40417  fourierdlem101  40424  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fourierdlem114  40437  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  elaa2lem  40450  etransclem23  40474  etransclem28  40479  etransclem32  40483  etransclem35  40486  etransclem48  40499  qndenserrnbllem  40514  rrnprjdstle  40521  ioorrnopnlem  40524  ioorrnopnxrlem  40526  salexct  40552  sge0fsum  40604  sge0supre  40606  sge0rnbnd  40610  sge0lefi  40615  sge0lessmpt  40616  sge0ltfirp  40617  sge0prle  40618  sge0resrnlem  40620  sge0le  40624  sge0split  40626  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0isum  40644  sge0xaddlem1  40650  sge0xaddlem2  40651  sge0xadd  40652  sge0reuz  40664  sge0reuzb  40665  meaunle  40681  meaiunlelem  40685  voliunsge0lem  40689  meaiuninc  40698  meaiininclem  40700  omeunle  40730  omeiunle  40731  omelesplit  40732  omeiunltfirp  40733  carageniuncllem2  40736  caratheodorylem2  40741  caragencmpl  40749  ovnlecvr  40772  ovncvrrp  40778  ovnsubaddlem1  40784  ovnsubadd  40786  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem5  40813  hoidmvle  40814  ovnhoilem1  40815  ovnlecvr2  40824  ovncvr2  40825  hoiqssbllem2  40837  hspmbllem2  40841  hspmbllem3  40842  ovnsplit  40862  ovolval5lem1  40866  vonioolem1  40894  vonioolem2  40895  vonicclem1  40897  vonicclem2  40898  pimconstlt1  40915  smflimlem2  40980  smflimlem4  40982  smfmullem1  40998  smfsuplem1  41017  smflimsuplem4  41029  smflimsuplem5  41030  iccpartltu  41361  iccpartleu  41364  pgrple2abl  42146  difmodm1lt  42317  nnpw2blen  42374  dignn0flhalflem1  42409