Theorem eqbrtrd 4300

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

Syntax hints:   -> wi 4   = wceq 1362   class class class wbr 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281

This theorem is referenced by:  eqbrtrrd  4302  somin2  5224  en1b  7365  domunsncan  7399  fodomfi  7578  hartogslem1  7744  wemaplem2  7749  infdifsn  7850  carddomi2  8128  cdaun  8329  cda1dif  8333  mapcdaen  8341  cdaxpdom  8346  cdafi  8347  cdainf  8349  carden  8703  alephsuc3  8732  fpwwe2lem6  8789  fpwwe2lem7  8790  inar1  8929  rankcf  8931  lbinfmle  10272  supmul  10285  rpnnen1lem3  10968  xrmin1  11136  xrmin2  11137  ifle  11154  qbtwnxr  11157  xltnegi  11173  xleadd1a  11203  xlt2add  11210  xlemul1a  11238  xov1plusxeqvd  11417  ubmelm1fzo  11606  ceim1l  11669  ceilm1lt  11670  ceille  11672  quoremz  11677  quoremnn0ALT  11679  modlt  11701  modeqmodmin  11751  seqf1olem1  11828  bernneq  11973  discr  11984  faclbnd2  12050  faclbnd4lem3  12054  hashun2  12129  hashfun  12182  ccatsymb  12264  lswccat0lsw  12271  sqrlem6  12720  sqrlem7  12721  rddif  12811  amgm2  12840  climconst  13004  rlimconst  13005  serclim0  13038  rlimcn1  13049  mulcn2  13056  reccn2  13057  o1mul  13075  o1rlimmul  13079  iserex  13117  climlec2  13119  iserge0  13121  climcau  13131  caucvgrlem  13133  caucvgr  13136  iseraltlem2  13143  iseraltlem3  13144  iseralt  13145  fsumabs  13246  o1fsum  13258  iserabs  13260  climfsum  13265  isumless  13290  climcndslem2  13295  divrcnv  13297  flo1  13299  supcvg  13300  georeclim  13314  geomulcvg  13318  cvgrat  13325  mertenslem1  13326  efcvgfsum  13353  eftlub  13375  eflegeo  13387  tanhlt1  13426  tanhbnd  13427  ef01bndlem  13450  sin01bnd  13451  cos01bnd  13452  cos01gt0  13457  ruclem2  13496  ruclem3  13497  ruclem9  13502  ruclem11  13504  ruclem12  13505  bitsfzolem  13612  bitsfzo  13613  bitsinv1lem  13619  sadcaddlem  13635  mulgcd  13712  eucalglt  13742  prmind2  13756  mulgcddvds  13772  isprm5  13780  divdenle  13809  nonsq  13819  pythagtriplem4  13868  pclem  13887  pcpremul  13892  pczdvds  13911  pcprmpw2  13930  qexpz  13945  prmreclem4  13962  prmreclem5  13963  4sqlem10  13990  ramtub  14055  ramub2  14057  natpropd  14868  catciso  14957  p0le  15195  acsdomd  15333  divsgrp  15715  f1otrspeq  15932  pmtrfrn  15943  pmtrfconj  15951  symggen  15955  psgnunilem4  15982  oddvds2  16046  odcau  16082  pgpfi  16083  pgpssslw  16092  sylow3lem4  16108  efgred2  16229  frgp0  16236  odadd2  16310  oddvdssubg  16316  ablfac1c  16545  ablfac1eu  16547  pgpfaclem3  16557  isabvd  16828  abvsubtri  16843  mplsubrg  17452  coe1sfi  17566  cyggic  17846  en2top  18431  1stcrest  18898  2ndcrest  18899  hausmapdom  18945  ufilen  19344  xmetrtri2  19772  prdsxmetlem  19784  bl2in  19816  xblcntrps  19826  xblcntr  19827  ssblps  19838  ssbl  19839  blssps  19840  blss  19841  blcld  19921  methaus  19936  metustexhalfOLD  19979  metustexhalf  19980  nrginvrcnlem  20112  nrginvrcn  20113  nmoi  20148  nmo0  20155  nmoid  20162  blcvx  20216  reperflem  20236  reconnlem2  20245  metdcnlem  20254  metdscn  20273  metnrmlem3  20278  mulc1cncf  20322  iccpnfhmeo  20358  cnheiborlem  20367  cnheibor  20368  lebnumii  20379  pcopt  20435  pcopt2  20436  pcoass  20437  nmoleub2lem  20510  nmoleub2lem3  20511  nmoleub2lem2  20512  ipcau2  20590  tchcphlem1  20591  trirn  20740  rrxdstprj1  20749  minveclem3  20757  ivthlem2  20777  ivthlem3  20778  ivth2  20780  ovollb  20803  ovolsslem  20808  ovollb2lem  20812  ovolctb  20814  ovoliunlem1  20826  ovolsca  20839  ovolicc1  20840  ovolicc2lem4  20844  nulmbl  20858  ioombl1lem4  20883  uniioovol  20900  uniioombllem3a  20905  uniioombllem4  20907  opnmbllem  20922  volcn  20927  volivth  20928  i1fadd  21014  i1fmul  21015  mbfi1fseqlem4  21037  mbfi1fseqlem5  21038  mbfi1fseqlem6  21039  itg2const2  21060  itg2seq  21061  itg2uba  21062  itg2split  21068  itg2monolem1  21069  itg2monolem3  21071  itg2i1fseq2  21075  itg2addlem  21077  itg2gt0  21079  itg2cnlem1  21080  itg2cnlem2  21081  itgless  21135  ibladdlem  21138  bddmulibl  21157  dveflem  21292  dvferm1lem  21297  dvferm2lem  21299  dvlip  21306  dvlipcn  21307  dvlip2  21308  dvle  21320  dvivthlem1  21321  lhop1lem  21326  dvcvx  21333  dvfsumabs  21336  dvfsumlem2  21340  dvfsumlem4  21342  dvfsumrlim2  21345  dvfsum2  21347  ftc1a  21350  ftc1lem4  21352  ftc1lem5  21353  deg1sub  21464  ply1divex  21492  deg1submon1p  21508  r1pdeglt  21514  dvdsq1p  21516  fta1glem2  21522  fta1g  21523  plyeq0lem  21562  dgrlt  21617  fta1lem  21657  aalioulem2  21683  aalioulem3  21684  aalioulem4  21685  aaliou3lem2  21693  aaliou3lem9  21700  taylply2  21717  ulmbdd  21747  ulmdvlem1  21749  mtest  21753  mtestbdd  21754  radcnvlem1  21762  radcnvle  21769  pserulm  21771  psercn  21775  pserdvlem2  21777  abelthlem2  21781  abelthlem5  21784  abelthlem7  21787  abelthlem8  21788  abelthlem9  21789  reeff1olem  21795  tangtx  21851  tanord  21878  efif1olem4  21885  logrnaddcl  21910  logcj  21939  logimul  21947  logneg2  21948  logdivlti  21953  divlogrlim  21964  logcnlem3  21973  logcnlem4  21974  efopn  21987  logtayllem  21988  logtayl  21989  cxpcn3lem  22069  cxpaddle  22074  abscxpbnd  22075  asinlem3  22150  asinneg  22165  asinsin  22171  atanlogaddlem  22192  atantan  22202  bndatandm  22208  atans2  22210  atantayl  22216  atantayl2  22217  atantayl3  22218  leibpi  22221  birthdaylem3  22231  rlimcnp  22243  efrlim  22247  cxplim  22249  cxp2lim  22254  cxploglim2  22256  divsqrsumo1  22261  jensenlem2  22265  amgm  22268  logdifbnd  22271  harmonicbnd4  22288  fsumharmonic  22289  ftalem1  22294  ftalem5  22298  basellem1  22302  basellem8  22309  ppip1le  22383  ppiltx  22399  sqff1o  22404  chtublem  22434  chpub  22443  logfaclbnd  22445  logfacrlim  22447  logexprlim  22448  mersenne  22450  bcmono  22500  bcmax  22501  bposlem2  22508  bposlem5  22511  lgslem3  22521  lgsquadlem1  22577  lgsquadlem2  22578  2sqblem  22600  chebbnd1  22605  chtppilimlem1  22606  chto1ub  22609  chpchtlim  22612  chpo1ubb  22614  rplogsumlem1  22617  rplogsumlem2  22618  rpvmasumlem  22620  dchrisumlem1  22622  dchrisumlem2  22623  dchrmusum2  22627  dchrvmasumlem2  22631  dchrvmasumlem3  22632  dchrvmasumiflem1  22634  dchrisum0flblem1  22641  dchrisum0fno1  22644  dchrisum0lem1b  22648  dchrisum0lem1  22649  dchrisum0lem2a  22650  dchrisum0lem2  22651  rplogsum  22660  mudivsum  22663  mulogsumlem  22664  mulog2sumlem1  22667  mulog2sumlem2  22668  vmalogdivsum2  22671  2vmadivsumlem  22673  selberglem2  22679  selberg2b  22685  logdivbnd  22689  selberg3lem1  22690  selberg3lem2  22691  selberg4lem1  22693  pntrmax  22697  pntrsumo1  22698  pntrlog2bndlem1  22710  pntrlog2bndlem2  22711  pntrlog2bndlem3  22712  pntrlog2bndlem4  22713  pntrlog2bndlem5  22714  pntrlog2bnd  22717  pntpbnd1a  22718  pntpbnd2  22720  pntibndlem2  22724  pntlemb  22730  pntlemg  22731  pntlemh  22732  pntlemr  22735  pntlemj  22736  pntlemf  22738  pntlemo  22740  pnt  22747  padicabv  22763  ostth2lem2  22767  ostth2lem3  22768  ostth3  22771  brbtwn2  22973  colinearalglem4  22977  nvmtri2  23882  nvabs  23883  nvge0  23884  nvlmle  23909  smcnlem  23914  nmblolbii  24021  blocnilem  24026  siii  24075  ubthlem2  24094  minvecolem3  24099  htthlem  24141  bcsiALT  24403  bcs3  24407  chscllem4  24865  0cnop  25205  0cnfn  25206  nmbdoplbi  25250  nmcoplbi  25254  nmophmi  25257  nmbdfnlbi  25275  nmcfnlbi  25278  nlelchi  25287  riesz1  25291  cnlnadjlem2  25294  nmopadjlei  25314  nmoptrii  25320  nmopcoi  25321  nmopcoadji  25327  unierri  25330  branmfn  25331  pjs14i  25436  hstle  25456  cdj3lem2b  25663  xlt2addrd  25875  eliccelico  25889  elicoelioo  25890  ltesubnnd  25913  archirngz  26029  archiabllem2c  26035  sqsscirc1  26191  tpr2rico  26195  esumcst  26367  measunl  26483  measiun  26485  eulerpartlemgc  26592  eulerpartlemb  26598  ballotlemsel1i  26742  ballotlemro  26752  sgnsub  26774  signsplypnf  26798  signsply0  26799  signsvtn  26832  signsvfnn  26834  lgamgulmlem2  26863  lgamgulmlem3  26864  lgamgulmlem5  26866  lgambdd  26870  lgamcvg2  26888  erdsze2lem1  26938  sinccvglem  27163  divcnvlin  27245  prodfclim1  27254  iprodefisum  27351  faclimlem2  27396  nodense  27676  nobnddown  27688  supadd  28259  ltflcei  28260  lxflflp1  28262  opnmbllem0  28268  mblfinlem2  28270  mblfinlem3  28271  ismblfin  28273  itg2addnclem  28284  itg2addnclem2  28285  itg2addnclem3  28286  itg2addnc  28287  ibladdnclem  28289  ftc1cnnclem  28306  ftc1cnnc  28307  ftc1anc  28316  fnemeet1  28428  geomcau  28496  prdsbnd  28533  cntotbnd  28536  heiborlem4  28554  rrndstprj2  28571  rrncmslem  28572  rrnequiv  28575  iccbnd  28580  lzenom  28950  icodiamlt  29003  irrapxlem2  29006  irrapxlem3  29007  irrapxlem5  29009  pellexlem2  29013  pell14qrgt0  29042  pellfundlb  29067  pellfundex  29069  pellfund14  29081  rmspecsqrnq  29089  jm2.24nn  29144  jm2.17a  29145  jm2.17b  29146  congabseq  29159  acongrep  29165  acongeq  29168  jm2.26lem3  29192  jm2.27a  29196  jm2.27c  29198  hbtlem2  29322  dgraaub  29347  idomodle  29403  fmul01  29603  fmul01lt1lem1  29607  fmul01lt1lem2  29608  climrec  29619  climsuse  29624  stoweidlem1  29639  stoweidlem11  29649  stoweidlem13  29651  stoweidlem14  29652  stoweidlem16  29654  stoweidlem21  29659  stoweidlem25  29663  stoweidlem26  29664  stoweidlem36  29674  stoweidlem38  29676  stoweidlem41  29679  stoweidlem42  29680  stoweidlem45  29683  stoweidlem48  29686  stoweidlem52  29690  stoweidlem62  29700  wallispilem3  29705  stirlinglem5  29716  stirlinglem6  29717  stirlinglem7  29718  stirlinglem10  29721  stirlinglem12  29723  stirlinglem15  29726  elfzom1elfzo  30060  pgrple2abel  30596  cvlcvr1  32554  cvrat3  32656  dalem25  32912  cdlema1N  33005  dalawlem3  33087  dalawlem4  33088  dalawlem5  33089  dalawlem6  33090  dalawlem7  33091  dalawlem9  33093  dalawlem11  33095  dalawlem12  33096  lhp2lt  33215  lhpmcvr  33237  4atexlemcnd  33286  lautj  33307  trlle  33398  trlval3  33401  trlval4  33402  cdleme0moN  33439  cdleme13  33486  cdleme15  33492  cdleme19b  33518  cdleme20e  33527  cdleme20j  33532  cdleme22e  33558  cdleme22eALTN  33559  cdleme26fALTN  33576  cdleme26f  33577  cdleme27N  33583  cdleme41sn3a  33647  cdleme46fsvlpq  33719  cdlemeg46vrg  33741  cdlemg4  33831  cdlemg7N  33840  cdlemg9a  33846  cdlemg11b  33856  cdlemg12a  33857  trljco  33954  tendoidcl  33983  tendococl  33986  tendopltp  33994  tendo0tp  34003  tendoicl  34010  cdlemi2  34033  cdlemk5a  34049  cdlemk5  34050  cdlemk12  34064  cdlemkole  34067  cdlemk14  34068  cdlemk12u  34086  cdlemk37  34128  cdlemk39s-id  34154  cdlemk49  34165  cdlemk39u1  34181  cdlemk39u  34182  dian0  34254  cdlemm10N  34333  cdlemn2  34410  cdlemn10  34421  dihord1  34433  dihord10  34438  dihmeetlem4preN  34521  dihmeetlem18N  34539  dihmeetlem20N  34541  dihjatc  34632  mapdcnvatN  34881