Theorem eqbrtrd 4476

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

Syntax hints:   -> wi 4   = wceq 1395   class class class wbr 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457

This theorem is referenced by:  eqbrtrrd  4478  somin2  5412  en1b  7602  domunsncan  7636  fodomfi  7817  hartogslem1  7985  wemaplem2  7990  infdifsn  8090  carddomi2  8368  cdaun  8569  cda1dif  8573  mapcdaen  8581  cdaxpdom  8586  cdafi  8587  cdainf  8589  carden  8943  alephsuc3  8972  fpwwe2lem6  9030  fpwwe2lem7  9031  inar1  9170  rankcf  9172  lbinfmle  10518  supmul  10531  rpnnen1lem3  11235  xrmin1  11403  xrmin2  11404  ifle  11421  qbtwnxr  11424  xltnegi  11440  xleadd1a  11470  xlt2add  11477  xlemul1a  11505  xov1plusxeqvd  11691  ubmelm1fzo  11911  flflp1  11947  ceim1l  11977  ceilm1lt  11978  ceille  11980  quoremz  11985  quoremnn0ALT  11987  modlt  12009  modeqmodmin  12059  seqf1olem1  12149  bernneq  12295  discr  12306  faclbnd2  12372  faclbnd4lem3  12376  hashun2  12454  hashfun  12499  ccatsymb  12609  ccatrn  12615  sqrlem6  13093  sqrlem7  13094  rddif  13185  amgm2  13214  climconst  13378  rlimconst  13379  serclim0  13412  rlimcn1  13423  mulcn2  13430  reccn2  13431  o1mul  13449  o1rlimmul  13453  iserex  13491  climlec2  13493  iserge0  13495  climcau  13505  caucvgrlem  13507  caucvgr  13510  iseraltlem2  13517  iseraltlem3  13518  iseralt  13519  fsumabs  13627  o1fsum  13639  iserabs  13641  climfsum  13646  isumless  13669  climcndslem2  13674  divrcnv  13676  flo1  13678  supcvg  13679  georeclim  13693  geomulcvg  13697  cvgrat  13704  mertenslem1  13705  prodfclim1  13714  efcvgfsum  13833  eftlub  13856  eflegeo  13868  tanhlt1  13907  tanhbnd  13908  ef01bndlem  13931  sin01bnd  13932  cos01bnd  13933  cos01gt0  13938  ruclem2  13977  ruclem3  13978  ruclem9  13983  ruclem11  13985  ruclem12  13986  bitsfzolem  14096  bitsfzo  14097  bitsinv1lem  14103  sadcaddlem  14119  mulgcd  14196  eucalglt  14226  prmind2  14240  mulgcddvds  14257  isprm5  14265  divdenle  14294  nonsq  14304  pythagtriplem4  14355  pclem  14374  pcpremul  14379  pczdvds  14398  pcprmpw2  14417  qexpz  14432  prmreclem4  14449  prmreclem5  14450  4sqlem10  14477  ramtub  14542  ramub2  14544  natpropd  15392  catciso  15513  p0le  15800  acsdomd  15938  qusgrp  16383  f1otrspeq  16599  pmtrfrn  16610  pmtrfconj  16618  symggen  16622  psgnunilem4  16649  oddvds2  16715  odcau  16751  pgpfi  16752  pgpssslw  16761  sylow3lem4  16777  efgred2  16898  frgp0  16905  odadd2  16982  oddvdssubg  16988  ablfac1c  17249  ablfac1eu  17251  pgpfaclem3  17261  isabvd  17596  abvsubtri  17611  mplsubrg  18229  coe1sfi  18379  cyggic  18738  mp2pm2mplem5  19438  en2top  19614  1stcrest  20080  2ndcrest  20081  hausmapdom  20127  ufilen  20557  xmetrtri2  20985  prdsxmetlem  20997  bl2in  21029  xblcntrps  21039  xblcntr  21040  ssblps  21051  ssbl  21052  blssps  21053  blss  21054  blcld  21134  methaus  21149  metustexhalfOLD  21192  metustexhalf  21193  nrginvrcnlem  21325  nrginvrcn  21326  nmoi  21361  nmo0  21368  nmoid  21375  blcvx  21429  reperflem  21449  reconnlem2  21458  metdcnlem  21467  metdscn  21486  metnrmlem3  21491  mulc1cncf  21535  iccpnfhmeo  21571  cnheiborlem  21580  cnheibor  21581  lebnumii  21592  pcopt  21648  pcopt2  21649  pcoass  21650  nmoleub2lem  21723  nmoleub2lem3  21724  nmoleub2lem2  21725  ipcau2  21803  tchcphlem1  21804  trirn  21953  rrxdstprj1  21962  minveclem3  21970  ivthlem2  21990  ivthlem3  21991  ivth2  21993  ovollb  22016  ovolsslem  22021  ovollb2lem  22025  ovolctb  22027  ovoliunlem1  22039  ovolsca  22052  ovolicc1  22053  ovolicc2lem4  22057  nulmbl  22072  ioombl1lem4  22097  uniioovol  22114  uniioombllem3a  22119  uniioombllem4  22121  opnmbllem  22136  volcn  22141  volivth  22142  i1fadd  22228  i1fmul  22229  mbfi1fseqlem4  22251  mbfi1fseqlem5  22252  mbfi1fseqlem6  22253  itg2const2  22274  itg2seq  22275  itg2uba  22276  itg2split  22282  itg2monolem1  22283  itg2monolem3  22285  itg2i1fseq2  22289  itg2addlem  22291  itg2gt0  22293  itg2cnlem1  22294  itg2cnlem2  22295  itgless  22349  ibladdlem  22352  bddmulibl  22371  dveflem  22506  dvferm1lem  22511  dvferm2lem  22513  dvlip  22520  dvlipcn  22521  dvlip2  22522  dvle  22534  dvivthlem1  22535  lhop1lem  22540  dvcvx  22547  dvfsumabs  22550  dvfsumlem2  22554  dvfsumlem4  22556  dvfsumrlim2  22559  dvfsum2  22561  ftc1a  22564  ftc1lem4  22566  ftc1lem5  22567  deg1sub  22635  ply1divex  22663  deg1submon1p  22679  r1pdeglt  22685  dvdsq1p  22687  fta1glem2  22693  fta1g  22694  plyeq0lem  22733  dgrlt  22789  fta1lem  22829  aalioulem2  22855  aalioulem3  22856  aalioulem4  22857  aaliou3lem2  22865  aaliou3lem9  22872  taylply2  22889  ulmbdd  22919  ulmdvlem1  22921  mtest  22925  mtestbdd  22926  radcnvlem1  22934  radcnvle  22941  pserulm  22943  psercn  22947  pserdvlem2  22949  abelthlem2  22953  abelthlem5  22956  abelthlem7  22959  abelthlem8  22960  abelthlem9  22961  reeff1olem  22967  tangtx  23024  tanord  23051  efif1olem4  23058  logrnaddcl  23088  logcj  23117  logimul  23125  logneg2  23126  logdivlti  23131  divlogrlim  23142  logcnlem3  23151  logcnlem4  23152  efopn  23165  logtayllem  23166  logtayl  23167  cxpcn3lem  23247  cxpaddle  23252  abscxpbnd  23253  asinlem3  23328  asinneg  23343  asinsin  23349  atanlogaddlem  23370  atantan  23380  bndatandm  23386  atans2  23388  atantayl  23394  atantayl2  23395  atantayl3  23396  leibpi  23399  birthdaylem3  23409  rlimcnp  23421  efrlim  23425  cxplim  23427  cxp2lim  23432  cxploglim2  23434  divsqrtsumo1  23439  jensenlem2  23443  amgm  23446  logdifbnd  23449  harmonicbnd4  23466  fsumharmonic  23467  ftalem1  23472  ftalem5  23476  basellem1  23480  basellem8  23487  ppip1le  23561  ppiltx  23577  sqff1o  23582  chtublem  23612  chpub  23621  logfaclbnd  23623  logfacrlim  23625  logexprlim  23626  mersenne  23628  bcmono  23678  bcmax  23679  bposlem2  23686  bposlem5  23689  lgslem3  23699  lgsquadlem1  23755  lgsquadlem2  23756  2sqblem  23778  chebbnd1  23783  chtppilimlem1  23784  chto1ub  23787  chpchtlim  23790  chpo1ubb  23792  rplogsumlem1  23795  rplogsumlem2  23796  rpvmasumlem  23798  dchrisumlem1  23800  dchrisumlem2  23801  dchrmusum2  23805  dchrvmasumlem2  23809  dchrvmasumlem3  23810  dchrvmasumiflem1  23812  dchrisum0flblem1  23819  dchrisum0fno1  23822  dchrisum0lem1b  23826  dchrisum0lem1  23827  dchrisum0lem2a  23828  dchrisum0lem2  23829  rplogsum  23838  mudivsum  23841  mulogsumlem  23842  mulog2sumlem1  23845  mulog2sumlem2  23846  vmalogdivsum2  23849  2vmadivsumlem  23851  selberglem2  23857  selberg2b  23863  logdivbnd  23867  selberg3lem1  23868  selberg3lem2  23869  selberg4lem1  23871  pntrmax  23875  pntrsumo1  23876  pntrlog2bndlem1  23888  pntrlog2bndlem2  23889  pntrlog2bndlem3  23890  pntrlog2bndlem4  23891  pntrlog2bndlem5  23892  pntrlog2bnd  23895  pntpbnd1a  23896  pntpbnd2  23898  pntibndlem2  23902  pntlemb  23908  pntlemg  23909  pntlemh  23910  pntlemr  23913  pntlemj  23914  pntlemf  23916  pntlemo  23918  pnt  23925  padicabv  23941  ostth2lem2  23945  ostth2lem3  23946  ostth3  23949  colperpexlem3  24232  mideulem2  24234  brbtwn2  24335  colinearalglem4  24339  nvmtri2  25702  nvabs  25703  nvge0  25704  nvlmle  25729  smcnlem  25734  nmblolbii  25841  blocnilem  25846  siii  25895  ubthlem2  25914  minvecolem3  25919  htthlem  25961  bcsiALT  26223  bcs3  26227  chscllem4  26685  0cnop  27025  0cnfn  27026  nmbdoplbi  27070  nmcoplbi  27074  nmophmi  27077  nmbdfnlbi  27095  nmcfnlbi  27098  nlelchi  27107  riesz1  27111  cnlnadjlem2  27114  nmopadjlei  27134  nmoptrii  27140  nmopcoi  27141  nmopcoadji  27147  unierri  27150  branmfn  27151  pjs14i  27256  hstle  27276  cdj3lem2b  27483  xlt2addrd  27735  eliccelico  27748  elicoelioo  27749  ltesubnnd  27772  archirngz  27893  archiabllem2c  27899  locfinref  28005  sqsscirc1  28051  tpr2rico  28055  esumcst  28235  esumgect  28262  esum2d  28265  measunl  28360  measiun  28362  omssubadd  28444  carsgsigalem  28458  carsgclctunlem2  28461  eulerpartlemgc  28498  eulerpartlemb  28504  ballotlemsel1i  28648  ballotlemro  28658  sgnsub  28680  signsplypnf  28704  signsply0  28705  signsvtn  28738  signsvfnn  28740  lgamgulmlem2  28769  lgamgulmlem3  28770  lgamgulmlem5  28772  lgambdd  28776  lgamcvg2  28794  erdsze2lem1  28844  sinccvglem  29235  divcnvlin  29336  iprodefisum  29342  faclimlem2  29387  nodense  29666  nobnddown  29678  supadd  30247  ltflcei  30248  opnmbllem0  30255  mblfinlem2  30257  mblfinlem3  30258  ismblfin  30260  itg2addnclem  30271  itg2addnclem2  30272  itg2addnclem3  30273  itg2addnc  30274  ibladdnclem  30276  ftc1cnnclem  30293  ftc1cnnc  30294  ftc1anc  30303  fnemeet1  30389  geomcau  30457  prdsbnd  30494  cntotbnd  30497  heiborlem4  30515  rrndstprj2  30532  rrncmslem  30533  rrnequiv  30536  iccbnd  30541  lzenom  30908  icodiamlt  30960  irrapxlem2  30963  irrapxlem3  30964  irrapxlem5  30966  pellexlem2  30970  pell14qrgt0  30999  pellfundlb  31024  pellfundex  31026  pellfund14  31038  rmspecsqrtnq  31046  jm2.24nn  31101  jm2.17a  31102  jm2.17b  31103  congabseq  31116  acongrep  31122  acongeq  31125  jm2.26lem3  31147  jm2.27a  31151  jm2.27c  31153  hbtlem2  31277  dgraaub  31301  idomodle  31357  lcmledvds  31409  hashnzfzclim  31431  binomcxplemfrat  31460  binomcxplemnotnn0  31465  suprnmpt  31654  dstregt0  31666  lefldiveq  31685  fzisoeu  31703  upbdrech  31708  ssfiunibd  31712  fzdifsuc2  31715  divge1  31716  ioondisj2  31728  iccshift  31761  iooshift  31765  fmul01  31777  fmul01lt1lem1  31781  fmul01lt1lem2  31782  fprodge1  31801  fprodle  31807  climrec  31812  climsuse  31817  mullimc  31825  mullimcf  31832  constlimc  31833  idlimc  31835  divcnvg  31836  limcperiod  31837  limcrecl  31838  lptioo2  31840  lptioo1  31841  islpcn  31848  lptre2pt  31849  limcleqr  31853  neglimc  31856  addlimc  31857  0ellimcdiv  31858  limclner  31860  sinaover2ne0  31871  cncfshift  31879  cncfperiod  31884  cncfioobdlem  31902  cncfioobd  31903  fperdvper  31918  dvdivbd  31923  dvbdfbdioolem1  31928  dvbdfbdioolem2  31929  ioodvbdlimc1lem1  31931  ioodvbdlimc1lem2  31932  ioodvbdlimc2lem  31934  dvnmul  31943  dvnprodlem1  31946  itgiccshift  31982  itgperiod  31983  stoweidlem1  31986  stoweidlem11  31996  stoweidlem13  31998  stoweidlem14  31999  stoweidlem16  32001  stoweidlem21  32006  stoweidlem25  32010  stoweidlem26  32011  stoweidlem36  32021  stoweidlem38  32023  stoweidlem41  32026  stoweidlem42  32027  stoweidlem45  32030  stoweidlem48  32033  stoweidlem52  32037  stoweidlem62  32047  wallispilem3  32052  stirlinglem5  32063  stirlinglem6  32064  stirlinglem7  32065  stirlinglem10  32068  stirlinglem12  32070  stirlinglem15  32073  dirkercncflem1  32088  fourierdlem10  32102  fourierdlem12  32104  fourierdlem15  32107  fourierdlem16  32108  fourierdlem19  32111  fourierdlem20  32112  fourierdlem21  32113  fourierdlem22  32114  fourierdlem24  32116  fourierdlem30  32122  fourierdlem37  32129  fourierdlem39  32131  fourierdlem40  32132  fourierdlem41  32133  fourierdlem42  32134  fourierdlem47  32139  fourierdlem48  32140  fourierdlem49  32141  fourierdlem50  32142  fourierdlem52  32144  fourierdlem54  32146  fourierdlem60  32152  fourierdlem61  32153  fourierdlem63  32155  fourierdlem64  32156  fourierdlem68  32160  fourierdlem71  32163  fourierdlem72  32164  fourierdlem73  32165  fourierdlem74  32166  fourierdlem75  32167  fourierdlem76  32168  fourierdlem77  32169  fourierdlem78  32170  fourierdlem79  32171  fourierdlem81  32173  fourierdlem82  32174  fourierdlem83  32175  fourierdlem84  32176  fourierdlem87  32179  fourierdlem92  32184  fourierdlem93  32185  fourierdlem94  32186  fourierdlem101  32193  fourierdlem102  32194  fourierdlem103  32195  fourierdlem104  32196  fourierdlem111  32203  fourierdlem112  32204  fourierdlem113  32205  fourierdlem114  32206  sqwvfoura  32214  sqwvfourb  32215  fouriersw  32217  elaa2lem  32219  etransclem23  32243  etransclem28  32248  etransclem32  32252  etransclem35  32255  etransclem48  32268  pgrple2abl  33102  cvlcvr1  35207  cvrat3  35309  dalem25  35565  cdlema1N  35658  dalawlem3  35740  dalawlem4  35741  dalawlem5  35742  dalawlem6  35743  dalawlem7  35744  dalawlem9  35746  dalawlem11  35748  dalawlem12  35749  lhp2lt  35868  lhpmcvr  35890  4atexlemcnd  35939  lautj  35960  trlle  36052  trlval3  36055  trlval4  36056  cdleme0moN  36093  cdleme13  36140  cdleme15  36146  cdleme19b  36173  cdleme20e  36182  cdleme20j  36187  cdleme22e  36213  cdleme22eALTN  36214  cdleme26fALTN  36231  cdleme26f  36232  cdleme27N  36238  cdleme41sn3a  36302  cdleme46fsvlpq  36374  cdlemeg46vrg  36396  cdlemg4  36486  cdlemg7N  36495  cdlemg9a  36501  cdlemg11b  36511  cdlemg12a  36512  trljco  36609  tendoidcl  36638  tendococl  36641  tendopltp  36649  tendo0tp  36658  tendoicl  36665  cdlemi2  36688  cdlemk5a  36704  cdlemk5  36705  cdlemk12  36719  cdlemkole  36722  cdlemk14  36723  cdlemk12u  36741  cdlemk37  36783  cdlemk39s-id  36809  cdlemk49  36820  cdlemk39u1  36836  cdlemk39u  36837  dian0  36909  cdlemm10N  36988  cdlemn2  37065  cdlemn10  37076  dihord1  37088  dihord10  37093  dihmeetlem4preN  37176  dihmeetlem18N  37194  dihmeetlem20N  37196  dihjatc  37287  mapdcnvatN  37536