Theorem eqbrtrd 4307

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

Syntax hints:   -> wi 4   = wceq 1369   class class class wbr 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288

This theorem is referenced by:  eqbrtrrd  4309  somin2  5231  en1b  7369  domunsncan  7403  fodomfi  7582  hartogslem1  7748  wemaplem2  7753  infdifsn  7854  carddomi2  8132  cdaun  8333  cda1dif  8337  mapcdaen  8345  cdaxpdom  8350  cdafi  8351  cdainf  8353  carden  8707  alephsuc3  8736  fpwwe2lem6  8794  fpwwe2lem7  8795  inar1  8934  rankcf  8936  lbinfmle  10277  supmul  10290  rpnnen1lem3  10973  xrmin1  11141  xrmin2  11142  ifle  11159  qbtwnxr  11162  xltnegi  11178  xleadd1a  11208  xlt2add  11215  xlemul1a  11243  xov1plusxeqvd  11423  ubmelm1fzo  11615  ceim1l  11678  ceilm1lt  11679  ceille  11681  quoremz  11686  quoremnn0ALT  11688  modlt  11710  modeqmodmin  11760  seqf1olem1  11837  bernneq  11982  discr  11993  faclbnd2  12059  faclbnd4lem3  12063  hashun2  12138  hashfun  12191  ccatsymb  12273  lswccat0lsw  12280  sqrlem6  12729  sqrlem7  12730  rddif  12820  amgm2  12849  climconst  13013  rlimconst  13014  serclim0  13047  rlimcn1  13058  mulcn2  13065  reccn2  13066  o1mul  13084  o1rlimmul  13088  iserex  13126  climlec2  13128  iserge0  13130  climcau  13140  caucvgrlem  13142  caucvgr  13145  iseraltlem2  13152  iseraltlem3  13153  iseralt  13154  fsumabs  13256  o1fsum  13268  iserabs  13270  climfsum  13275  isumless  13300  climcndslem2  13305  divrcnv  13307  flo1  13309  supcvg  13310  georeclim  13324  geomulcvg  13328  cvgrat  13335  mertenslem1  13336  efcvgfsum  13363  eftlub  13385  eflegeo  13397  tanhlt1  13436  tanhbnd  13437  ef01bndlem  13460  sin01bnd  13461  cos01bnd  13462  cos01gt0  13467  ruclem2  13506  ruclem3  13507  ruclem9  13512  ruclem11  13514  ruclem12  13515  bitsfzolem  13622  bitsfzo  13623  bitsinv1lem  13629  sadcaddlem  13645  mulgcd  13722  eucalglt  13752  prmind2  13766  mulgcddvds  13782  isprm5  13790  divdenle  13819  nonsq  13829  pythagtriplem4  13878  pclem  13897  pcpremul  13902  pczdvds  13921  pcprmpw2  13940  qexpz  13955  prmreclem4  13972  prmreclem5  13973  4sqlem10  14000  ramtub  14065  ramub2  14067  natpropd  14878  catciso  14967  p0le  15205  acsdomd  15343  divsgrp  15727  f1otrspeq  15944  pmtrfrn  15955  pmtrfconj  15963  symggen  15967  psgnunilem4  15994  oddvds2  16058  odcau  16094  pgpfi  16095  pgpssslw  16104  sylow3lem4  16120  efgred2  16241  frgp0  16248  odadd2  16322  oddvdssubg  16328  ablfac1c  16562  ablfac1eu  16564  pgpfaclem3  16574  isabvd  16885  abvsubtri  16900  mplsubrg  17499  coe1sfi  17648  cyggic  17985  en2top  18570  1stcrest  19037  2ndcrest  19038  hausmapdom  19084  ufilen  19483  xmetrtri2  19911  prdsxmetlem  19923  bl2in  19955  xblcntrps  19965  xblcntr  19966  ssblps  19977  ssbl  19978  blssps  19979  blss  19980  blcld  20060  methaus  20075  metustexhalfOLD  20118  metustexhalf  20119  nrginvrcnlem  20251  nrginvrcn  20252  nmoi  20287  nmo0  20294  nmoid  20301  blcvx  20355  reperflem  20375  reconnlem2  20384  metdcnlem  20393  metdscn  20412  metnrmlem3  20417  mulc1cncf  20461  iccpnfhmeo  20497  cnheiborlem  20506  cnheibor  20507  lebnumii  20518  pcopt  20574  pcopt2  20575  pcoass  20576  nmoleub2lem  20649  nmoleub2lem3  20650  nmoleub2lem2  20651  ipcau2  20729  tchcphlem1  20730  trirn  20879  rrxdstprj1  20888  minveclem3  20896  ivthlem2  20916  ivthlem3  20917  ivth2  20919  ovollb  20942  ovolsslem  20947  ovollb2lem  20951  ovolctb  20953  ovoliunlem1  20965  ovolsca  20978  ovolicc1  20979  ovolicc2lem4  20983  nulmbl  20997  ioombl1lem4  21022  uniioovol  21039  uniioombllem3a  21044  uniioombllem4  21046  opnmbllem  21061  volcn  21066  volivth  21067  i1fadd  21153  i1fmul  21154  mbfi1fseqlem4  21176  mbfi1fseqlem5  21177  mbfi1fseqlem6  21178  itg2const2  21199  itg2seq  21200  itg2uba  21201  itg2split  21207  itg2monolem1  21208  itg2monolem3  21210  itg2i1fseq2  21214  itg2addlem  21216  itg2gt0  21218  itg2cnlem1  21219  itg2cnlem2  21220  itgless  21274  ibladdlem  21277  bddmulibl  21296  dveflem  21431  dvferm1lem  21436  dvferm2lem  21438  dvlip  21445  dvlipcn  21446  dvlip2  21447  dvle  21459  dvivthlem1  21460  lhop1lem  21465  dvcvx  21472  dvfsumabs  21475  dvfsumlem2  21479  dvfsumlem4  21481  dvfsumrlim2  21484  dvfsum2  21486  ftc1a  21489  ftc1lem4  21491  ftc1lem5  21492  deg1sub  21560  ply1divex  21588  deg1submon1p  21604  r1pdeglt  21610  dvdsq1p  21612  fta1glem2  21618  fta1g  21619  plyeq0lem  21658  dgrlt  21713  fta1lem  21753  aalioulem2  21779  aalioulem3  21780  aalioulem4  21781  aaliou3lem2  21789  aaliou3lem9  21796  taylply2  21813  ulmbdd  21843  ulmdvlem1  21845  mtest  21849  mtestbdd  21850  radcnvlem1  21858  radcnvle  21865  pserulm  21867  psercn  21871  pserdvlem2  21873  abelthlem2  21877  abelthlem5  21880  abelthlem7  21883  abelthlem8  21884  abelthlem9  21885  reeff1olem  21891  tangtx  21947  tanord  21974  efif1olem4  21981  logrnaddcl  22006  logcj  22035  logimul  22043  logneg2  22044  logdivlti  22049  divlogrlim  22060  logcnlem3  22069  logcnlem4  22070  efopn  22083  logtayllem  22084  logtayl  22085  cxpcn3lem  22165  cxpaddle  22170  abscxpbnd  22171  asinlem3  22246  asinneg  22261  asinsin  22267  atanlogaddlem  22288  atantan  22298  bndatandm  22304  atans2  22306  atantayl  22312  atantayl2  22313  atantayl3  22314  leibpi  22317  birthdaylem3  22327  rlimcnp  22339  efrlim  22343  cxplim  22345  cxp2lim  22350  cxploglim2  22352  divsqrsumo1  22357  jensenlem2  22361  amgm  22364  logdifbnd  22367  harmonicbnd4  22384  fsumharmonic  22385  ftalem1  22390  ftalem5  22394  basellem1  22398  basellem8  22405  ppip1le  22479  ppiltx  22495  sqff1o  22500  chtublem  22530  chpub  22539  logfaclbnd  22541  logfacrlim  22543  logexprlim  22544  mersenne  22546  bcmono  22596  bcmax  22597  bposlem2  22604  bposlem5  22607  lgslem3  22617  lgsquadlem1  22673  lgsquadlem2  22674  2sqblem  22696  chebbnd1  22701  chtppilimlem1  22702  chto1ub  22705  chpchtlim  22708  chpo1ubb  22710  rplogsumlem1  22713  rplogsumlem2  22714  rpvmasumlem  22716  dchrisumlem1  22718  dchrisumlem2  22719  dchrmusum2  22723  dchrvmasumlem2  22727  dchrvmasumlem3  22728  dchrvmasumiflem1  22730  dchrisum0flblem1  22737  dchrisum0fno1  22740  dchrisum0lem1b  22744  dchrisum0lem1  22745  dchrisum0lem2a  22746  dchrisum0lem2  22747  rplogsum  22756  mudivsum  22759  mulogsumlem  22760  mulog2sumlem1  22763  mulog2sumlem2  22764  vmalogdivsum2  22767  2vmadivsumlem  22769  selberglem2  22775  selberg2b  22781  logdivbnd  22785  selberg3lem1  22786  selberg3lem2  22787  selberg4lem1  22789  pntrmax  22793  pntrsumo1  22794  pntrlog2bndlem1  22806  pntrlog2bndlem2  22807  pntrlog2bndlem3  22808  pntrlog2bndlem4  22809  pntrlog2bndlem5  22810  pntrlog2bnd  22813  pntpbnd1a  22814  pntpbnd2  22816  pntibndlem2  22820  pntlemb  22826  pntlemg  22827  pntlemh  22828  pntlemr  22831  pntlemj  22832  pntlemf  22834  pntlemo  22836  pnt  22843  padicabv  22859  ostth2lem2  22863  ostth2lem3  22864  ostth3  22867  brbtwn2  23119  colinearalglem4  23123  nvmtri2  24028  nvabs  24029  nvge0  24030  nvlmle  24055  smcnlem  24060  nmblolbii  24167  blocnilem  24172  siii  24221  ubthlem2  24240  minvecolem3  24245  htthlem  24287  bcsiALT  24549  bcs3  24553  chscllem4  25011  0cnop  25351  0cnfn  25352  nmbdoplbi  25396  nmcoplbi  25400  nmophmi  25403  nmbdfnlbi  25421  nmcfnlbi  25424  nlelchi  25433  riesz1  25437  cnlnadjlem2  25440  nmopadjlei  25460  nmoptrii  25466  nmopcoi  25467  nmopcoadji  25473  unierri  25476  branmfn  25477  pjs14i  25582  hstle  25602  cdj3lem2b  25809  xlt2addrd  26019  eliccelico  26035  elicoelioo  26036  ltesubnnd  26059  archirngz  26174  archiabllem2c  26180  sqsscirc1  26307  tpr2rico  26311  esumcst  26483  measunl  26599  measiun  26601  eulerpartlemgc  26714  eulerpartlemb  26720  ballotlemsel1i  26864  ballotlemro  26874  sgnsub  26896  signsplypnf  26920  signsply0  26921  signsvtn  26954  signsvfnn  26956  lgamgulmlem2  26985  lgamgulmlem3  26986  lgamgulmlem5  26988  lgambdd  26992  lgamcvg2  27010  erdsze2lem1  27060  sinccvglem  27286  divcnvlin  27368  prodfclim1  27377  iprodefisum  27474  faclimlem2  27519  nodense  27799  nobnddown  27811  supadd  28389  ltflcei  28390  lxflflp1  28392  opnmbllem0  28398  mblfinlem2  28400  mblfinlem3  28401  ismblfin  28403  itg2addnclem  28414  itg2addnclem2  28415  itg2addnclem3  28416  itg2addnc  28417  ibladdnclem  28419  ftc1cnnclem  28436  ftc1cnnc  28437  ftc1anc  28446  fnemeet1  28558  geomcau  28626  prdsbnd  28663  cntotbnd  28666  heiborlem4  28684  rrndstprj2  28701  rrncmslem  28702  rrnequiv  28705  iccbnd  28710  lzenom  29079  icodiamlt  29132  irrapxlem2  29135  irrapxlem3  29136  irrapxlem5  29138  pellexlem2  29142  pell14qrgt0  29171  pellfundlb  29196  pellfundex  29198  pellfund14  29210  rmspecsqrnq  29218  jm2.24nn  29273  jm2.17a  29274  jm2.17b  29275  congabseq  29288  acongrep  29294  acongeq  29297  jm2.26lem3  29321  jm2.27a  29325  jm2.27c  29327  hbtlem2  29451  dgraaub  29476  idomodle  29532  fmul01  29732  fmul01lt1lem1  29736  fmul01lt1lem2  29737  climrec  29747  climsuse  29752  stoweidlem1  29767  stoweidlem11  29777  stoweidlem13  29779  stoweidlem14  29780  stoweidlem16  29782  stoweidlem21  29787  stoweidlem25  29791  stoweidlem26  29792  stoweidlem36  29802  stoweidlem38  29804  stoweidlem41  29807  stoweidlem42  29808  stoweidlem45  29811  stoweidlem48  29814  stoweidlem52  29818  stoweidlem62  29828  wallispilem3  29833  stirlinglem5  29844  stirlinglem6  29845  stirlinglem7  29846  stirlinglem10  29849  stirlinglem12  29851  stirlinglem15  29854  elfzom1elfzo  30188  pgrple2abel  30737  cvlcvr1  32877  cvrat3  32979  dalem25  33235  cdlema1N  33328  dalawlem3  33410  dalawlem4  33411  dalawlem5  33412  dalawlem6  33413  dalawlem7  33414  dalawlem9  33416  dalawlem11  33418  dalawlem12  33419  lhp2lt  33538  lhpmcvr  33560  4atexlemcnd  33609  lautj  33630  trlle  33721  trlval3  33724  trlval4  33725  cdleme0moN  33762  cdleme13  33809  cdleme15  33815  cdleme19b  33841  cdleme20e  33850  cdleme20j  33855  cdleme22e  33881  cdleme22eALTN  33882  cdleme26fALTN  33899  cdleme26f  33900  cdleme27N  33906  cdleme41sn3a  33970  cdleme46fsvlpq  34042  cdlemeg46vrg  34064  cdlemg4  34154  cdlemg7N  34163  cdlemg9a  34169  cdlemg11b  34179  cdlemg12a  34180  trljco  34277  tendoidcl  34306  tendococl  34309  tendopltp  34317  tendo0tp  34326  tendoicl  34333  cdlemi2  34356  cdlemk5a  34372  cdlemk5  34373  cdlemk12  34387  cdlemkole  34390  cdlemk14  34391  cdlemk12u  34409  cdlemk37  34451  cdlemk39s-id  34477  cdlemk49  34488  cdlemk39u1  34504  cdlemk39u  34505  dian0  34577  cdlemm10N  34656  cdlemn2  34733  cdlemn10  34744  dihord1  34756  dihord10  34761  dihmeetlem4preN  34844  dihmeetlem18N  34862  dihmeetlem20N  34864  dihjatc  34955  mapdcnvatN  35204