Theorem eqbrtrd 4415

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

Syntax hints:   -> wi 4   = wceq 1405   class class class wbr 4395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-br 4396

This theorem is referenced by:  eqbrtrrd  4417  somin2  5223  en1b  7621  domunsncan  7655  fodomfi  7833  hartogslem1  8001  wemaplem2  8006  infdifsn  8106  carddomi2  8383  cdaun  8584  cda1dif  8588  mapcdaen  8596  cdaxpdom  8601  cdafi  8602  cdainf  8604  carden  8958  alephsuc3  8987  fpwwe2lem6  9043  fpwwe2lem7  9044  inar1  9183  rankcf  9185  lbinfmle  10538  supmul  10551  rpnnen1lem3  11255  xrmin1  11431  xrmin2  11432  ifle  11449  qbtwnxr  11452  xltnegi  11468  xleadd1a  11498  xlt2add  11505  xlemul1a  11533  xov1plusxeqvd  11720  ubmelm1fzo  11945  flflp1  11981  ceim1l  12012  ceilm1lt  12013  ceille  12015  quoremz  12020  quoremnn0ALT  12022  modlt  12045  modeqmodmin  12097  seqf1olem1  12190  bernneq  12336  discr  12347  faclbnd2  12413  faclbnd4lem3  12417  hashun2  12499  hashfun  12544  ccatsymb  12654  ccatrn  12660  sqrlem6  13230  sqrlem7  13231  rddif  13322  amgm2  13351  climconst  13515  rlimconst  13516  serclim0  13549  rlimcn1  13560  mulcn2  13567  reccn2  13568  o1mul  13586  o1rlimmul  13590  iserex  13628  climlec2  13630  iserge0  13632  climcau  13642  caucvgrlem  13644  caucvgr  13647  iseraltlem2  13654  iseraltlem3  13655  iseralt  13656  fsumabs  13766  o1fsum  13778  iserabs  13780  climfsum  13785  isumless  13808  climcndslem2  13813  divrcnv  13815  flo1  13817  supcvg  13819  georeclim  13833  geomulcvg  13837  cvgrat  13844  mertenslem1  13845  prodfclim1  13854  efcvgfsum  14030  eftlub  14053  eflegeo  14065  tanhlt1  14104  tanhbnd  14105  ef01bndlem  14128  sin01bnd  14129  cos01bnd  14130  cos01gt0  14135  ruclem2  14174  ruclem3  14175  ruclem9  14180  ruclem11  14182  ruclem12  14183  bitsfzolem  14293  bitsfzo  14294  bitsinv1lem  14300  sadcaddlem  14316  mulgcd  14393  eucalglt  14423  prmind2  14437  mulgcddvds  14454  isprm5  14462  divdenle  14491  nonsq  14501  pythagtriplem4  14552  pclem  14571  pcpremul  14576  pczdvds  14595  pcprmpw2  14614  qexpz  14629  prmreclem4  14646  prmreclem5  14647  4sqlem10  14674  ramtub  14739  ramub2  14741  natpropd  15589  catciso  15710  p0le  15997  acsdomd  16135  qusgrp  16580  f1otrspeq  16796  pmtrfrn  16807  pmtrfconj  16815  symggen  16819  psgnunilem4  16846  oddvds2  16912  odcau  16948  pgpfi  16949  pgpssslw  16958  sylow3lem4  16974  efgred2  17095  frgp0  17102  odadd2  17179  oddvdssubg  17185  ablfac1c  17442  ablfac1eu  17444  pgpfaclem3  17454  isabvd  17789  abvsubtri  17804  mplsubrg  18422  coe1sfi  18572  cyggic  18909  mp2pm2mplem5  19603  en2top  19779  1stcrest  20246  2ndcrest  20247  hausmapdom  20293  ufilen  20723  xmetrtri2  21151  prdsxmetlem  21163  bl2in  21195  xblcntrps  21205  xblcntr  21206  ssblps  21217  ssbl  21218  blssps  21219  blss  21220  blcld  21300  methaus  21315  metustexhalfOLD  21358  metustexhalf  21359  nrginvrcnlem  21491  nrginvrcn  21492  nmoi  21527  nmo0  21534  nmoid  21541  blcvx  21595  reperflem  21615  reconnlem2  21624  metdcnlem  21633  metdscn  21652  metnrmlem3  21657  mulc1cncf  21701  iccpnfhmeo  21737  cnheiborlem  21746  cnheibor  21747  lebnumii  21758  pcopt  21814  pcopt2  21815  pcoass  21816  nmoleub2lem  21889  nmoleub2lem3  21890  nmoleub2lem2  21891  ipcau2  21969  tchcphlem1  21970  trirn  22119  rrxdstprj1  22128  minveclem3  22136  ivthlem2  22156  ivthlem3  22157  ivth2  22159  ovollb  22182  ovolsslem  22187  ovollb2lem  22191  ovolctb  22193  ovoliunlem1  22205  ovolsca  22218  ovolicc1  22219  ovolicc2lem4  22223  nulmbl  22238  ioombl1lem4  22263  uniioovol  22280  uniioombllem3a  22285  uniioombllem4  22287  opnmbllem  22302  volcn  22307  volivth  22308  i1fadd  22394  i1fmul  22395  mbfi1fseqlem4  22417  mbfi1fseqlem5  22418  mbfi1fseqlem6  22419  itg2const2  22440  itg2seq  22441  itg2uba  22442  itg2split  22448  itg2monolem1  22449  itg2monolem3  22451  itg2i1fseq2  22455  itg2addlem  22457  itg2gt0  22459  itg2cnlem1  22460  itg2cnlem2  22461  itgless  22515  ibladdlem  22518  bddmulibl  22537  dveflem  22672  dvferm1lem  22677  dvferm2lem  22679  dvlip  22686  dvlipcn  22687  dvlip2  22688  dvle  22700  dvivthlem1  22701  lhop1lem  22706  dvcvx  22713  dvfsumabs  22716  dvfsumlem2  22720  dvfsumlem4  22722  dvfsumrlim2  22725  dvfsum2  22727  ftc1a  22730  ftc1lem4  22732  ftc1lem5  22733  deg1sub  22801  ply1divex  22829  deg1submon1p  22845  r1pdeglt  22851  dvdsq1p  22853  fta1glem2  22859  fta1g  22860  plyeq0lem  22899  dgrlt  22955  fta1lem  22995  aalioulem2  23021  aalioulem3  23022  aalioulem4  23023  aaliou3lem2  23031  aaliou3lem9  23038  taylply2  23055  ulmbdd  23085  ulmdvlem1  23087  mtest  23091  mtestbdd  23092  radcnvlem1  23100  radcnvle  23107  pserulm  23109  psercn  23113  pserdvlem2  23115  abelthlem2  23119  abelthlem5  23122  abelthlem7  23125  abelthlem8  23126  abelthlem9  23127  reeff1olem  23133  tangtx  23190  tanord  23217  efif1olem4  23224  logrnaddcl  23254  logcj  23285  logimul  23293  logneg2  23294  logdivlti  23299  divlogrlim  23310  logcnlem3  23319  logcnlem4  23320  efopn  23333  logtayllem  23334  logtayl  23335  cxpcn3lem  23417  cxpaddle  23422  abscxpbnd  23423  asinlem3  23527  asinneg  23542  asinsin  23548  atanlogaddlem  23569  atantan  23579  bndatandm  23585  atans2  23587  atantayl  23593  atantayl2  23594  atantayl3  23595  leibpi  23598  birthdaylem3  23609  rlimcnp  23621  efrlim  23625  cxplim  23627  cxp2lim  23632  cxploglim2  23634  divsqrtsumo1  23639  jensenlem2  23643  amgm  23646  logdifbnd  23649  harmonicbnd4  23666  fsumharmonic  23667  lgamgulmlem2  23685  lgamgulmlem3  23686  lgamgulmlem5  23688  lgambdd  23692  lgamcvg2  23710  ftalem1  23727  ftalem5  23731  basellem1  23735  basellem8  23742  ppip1le  23816  ppiltx  23832  sqff1o  23837  chtublem  23867  chpub  23876  logfaclbnd  23878  logfacrlim  23880  logexprlim  23881  mersenne  23883  bcmono  23933  bcmax  23934  bposlem2  23941  bposlem5  23944  lgslem3  23954  lgsquadlem1  24010  lgsquadlem2  24011  2sqblem  24033  chebbnd1  24038  chtppilimlem1  24039  chto1ub  24042  chpchtlim  24045  chpo1ubb  24047  rplogsumlem1  24050  rplogsumlem2  24051  rpvmasumlem  24053  dchrisumlem1  24055  dchrisumlem2  24056  dchrmusum2  24060  dchrvmasumlem2  24064  dchrvmasumlem3  24065  dchrvmasumiflem1  24067  dchrisum0flblem1  24074  dchrisum0fno1  24077  dchrisum0lem1b  24081  dchrisum0lem1  24082  dchrisum0lem2a  24083  dchrisum0lem2  24084  rplogsum  24093  mudivsum  24096  mulogsumlem  24097  mulog2sumlem1  24100  mulog2sumlem2  24101  vmalogdivsum2  24104  2vmadivsumlem  24106  selberglem2  24112  selberg2b  24118  logdivbnd  24122  selberg3lem1  24123  selberg3lem2  24124  selberg4lem1  24126  pntrmax  24130  pntrsumo1  24131  pntrlog2bndlem1  24143  pntrlog2bndlem2  24144  pntrlog2bndlem3  24145  pntrlog2bndlem4  24146  pntrlog2bndlem5  24147  pntrlog2bnd  24150  pntpbnd1a  24151  pntpbnd2  24153  pntibndlem2  24157  pntlemb  24163  pntlemg  24164  pntlemh  24165  pntlemr  24168  pntlemj  24169  pntlemf  24171  pntlemo  24173  pnt  24180  padicabv  24196  ostth2lem2  24200  ostth2lem3  24201  ostth3  24204  colperpexlem3  24492  mideulem2  24494  lnperpex  24559  trgcopy  24560  brbtwn2  24625  colinearalglem4  24629  nvmtri2  25989  nvabs  25990  nvge0  25991  nvlmle  26016  smcnlem  26021  nmblolbii  26128  blocnilem  26133  siii  26182  ubthlem2  26201  minvecolem3  26206  htthlem  26248  bcsiALT  26510  bcs3  26514  chscllem4  26972  0cnop  27311  0cnfn  27312  nmbdoplbi  27356  nmcoplbi  27360  nmophmi  27363  nmbdfnlbi  27381  nmcfnlbi  27384  nlelchi  27393  riesz1  27397  cnlnadjlem2  27400  nmopadjlei  27420  nmoptrii  27426  nmopcoi  27427  nmopcoadji  27433  unierri  27436  branmfn  27437  pjs14i  27542  hstle  27562  cdj3lem2b  27769  xlt2addrd  28020  eliccelico  28036  elicoelioo  28037  ltesubnnd  28064  archirngz  28185  archiabllem2c  28191  locfinref  28297  sqsscirc1  28343  tpr2rico  28347  esumcst  28510  esumgect  28537  esum2d  28540  measunl  28664  measiun  28666  omssubadd  28748  carsgsigalem  28763  carsgclctunlem2  28767  pmeasmono  28772  eulerpartlemgc  28807  eulerpartlemb  28813  ballotlemsel1i  28957  ballotlemro  28967  sgnsub  28989  signsplypnf  29013  signsply0  29014  signsvtn  29047  signsvfnn  29049  erdsze2lem1  29500  sinccvglem  29890  divcnvlin  29940  iprodefisum  29950  faclimlem2  29953  nodense  30149  nobnddown  30161  fnemeet1  30594  supadd  31414  ltflcei  31415  opnmbllem0  31422  mblfinlem2  31424  mblfinlem3  31425  ismblfin  31427  itg2addnclem  31439  itg2addnclem2  31440  itg2addnclem3  31441  itg2addnc  31442  ibladdnclem  31444  ftc1cnnclem  31461  ftc1cnnc  31462  ftc1anc  31471  geomcau  31534  prdsbnd  31571  cntotbnd  31574  heiborlem4  31592  rrndstprj2  31609  rrncmslem  31610  rrnequiv  31613  iccbnd  31618  cvlcvr1  32357  cvrat3  32459  dalem25  32715  cdlema1N  32808  dalawlem3  32890  dalawlem4  32891  dalawlem5  32892  dalawlem6  32893  dalawlem7  32894  dalawlem9  32896  dalawlem11  32898  dalawlem12  32899  lhp2lt  33018  lhpmcvr  33040  4atexlemcnd  33089  lautj  33110  trlle  33202  trlval3  33205  trlval4  33206  cdleme0moN  33243  cdleme13  33290  cdleme15  33296  cdleme19b  33323  cdleme20e  33332  cdleme20j  33337  cdleme22e  33363  cdleme22eALTN  33364  cdleme26fALTN  33381  cdleme26f  33382  cdleme27N  33388  cdleme41sn3a  33452  cdleme46fsvlpq  33524  cdlemeg46vrg  33546  cdlemg4  33636  cdlemg7N  33645  cdlemg9a  33651  cdlemg11b  33661  cdlemg12a  33662  trljco  33759  tendoidcl  33788  tendococl  33791  tendopltp  33799  tendo0tp  33808  tendoicl  33815  cdlemi2  33838  cdlemk5a  33854  cdlemk5  33855  cdlemk12  33869  cdlemkole  33872  cdlemk14  33873  cdlemk12u  33891  cdlemk37  33933  cdlemk39s-id  33959  cdlemk49  33970  cdlemk39u1  33986  cdlemk39u  33987  dian0  34059  cdlemm10N  34138  cdlemn2  34215  cdlemn10  34226  dihord1  34238  dihord10  34243  dihmeetlem4preN  34326  dihmeetlem18N  34344  dihmeetlem20N  34346  dihjatc  34437  mapdcnvatN  34686  lzenom  35064  icodiamlt  35117  irrapxlem2  35120  irrapxlem3  35121  irrapxlem5  35123  pellexlem2  35127  pell14qrgt0  35156  pellfundlb  35181  pellfundex  35183  pellfund14  35195  rmspecsqrtnq  35203  jm2.24nn  35258  jm2.17a  35259  jm2.17b  35260  congabseq  35273  acongrep  35279  acongeq  35282  jm2.26lem3  35305  jm2.27a  35309  jm2.27c  35311  hbtlem2  35437  dgraaub  35461  idomodle  35517  relexpxpmin  35696  frege102d  35733  lcmledvds  36053  hashnzfzclim  36075  binomcxplemfrat  36104  binomcxplemnotnn0  36109  suprnmpt  36826  dstregt0  36837  lefldiveq  36854  fzisoeu  36869  upbdrech  36874  ssfiunibd  36878  fzdifsuc2  36881  divge1  36882  ioondisj2  36894  iccshift  36926  iooshift  36930  fmul01  36942  fmul01lt1lem1  36946  fmul01lt1lem2  36947  fprodge1  36966  fprodle  36972  climrec  36977  climsuse  36982  mullimc  36990  mullimcf  36997  constlimc  36998  idlimc  37000  divcnvg  37001  limcperiod  37002  limcrecl  37003  lptioo2  37005  lptioo1  37006  islpcn  37013  lptre2pt  37014  limcleqr  37018  neglimc  37021  addlimc  37022  0ellimcdiv  37023  limclner  37025  sinaover2ne0  37036  cncfshift  37044  cncfperiod  37049  cncfioobdlem  37067  cncfioobd  37068  fperdvper  37083  dvdivbd  37088  dvbdfbdioolem1  37093  dvbdfbdioolem2  37094  ioodvbdlimc1lem1  37096  ioodvbdlimc1lem2  37097  ioodvbdlimc2lem  37099  dvnmul  37108  dvnprodlem1  37111  itgiccshift  37147  itgperiod  37148  stoweidlem1  37151  stoweidlem11  37161  stoweidlem13  37163  stoweidlem14  37164  stoweidlem16  37166  stoweidlem21  37171  stoweidlem25  37175  stoweidlem26  37176  stoweidlem36  37186  stoweidlem38  37188  stoweidlem41  37191  stoweidlem42  37192  stoweidlem45  37195  stoweidlem48  37198  stoweidlem52  37202  stoweidlem62  37212  wallispilem3  37217  stirlinglem5  37228  stirlinglem6  37229  stirlinglem7  37230  stirlinglem10  37233  stirlinglem12  37235  stirlinglem15  37238  dirkercncflem1  37253  fourierdlem10  37267  fourierdlem12  37269  fourierdlem15  37272  fourierdlem16  37273  fourierdlem19  37276  fourierdlem20  37277  fourierdlem21  37278  fourierdlem22  37279  fourierdlem24  37281  fourierdlem30  37287  fourierdlem37  37294  fourierdlem39  37296  fourierdlem40  37297  fourierdlem41  37298  fourierdlem42  37299  fourierdlem47  37304  fourierdlem48  37305  fourierdlem49  37306  fourierdlem50  37307  fourierdlem52  37309  fourierdlem54  37311  fourierdlem60  37317  fourierdlem61  37318  fourierdlem63  37320  fourierdlem64  37321  fourierdlem68  37325  fourierdlem71  37328  fourierdlem72  37329  fourierdlem73  37330  fourierdlem74  37331  fourierdlem75  37332  fourierdlem76  37333  fourierdlem77  37334  fourierdlem78  37335  fourierdlem79  37336  fourierdlem81  37338  fourierdlem82  37339  fourierdlem83  37340  fourierdlem84  37341  fourierdlem87  37344  fourierdlem92  37349  fourierdlem93  37350  fourierdlem94  37351  fourierdlem101  37358  fourierdlem102  37359  fourierdlem103  37360  fourierdlem104  37361  fourierdlem111  37368  fourierdlem112  37369  fourierdlem113  37370  fourierdlem114  37371  sqwvfoura  37379  sqwvfourb  37380  fouriersw  37382  elaa2lem  37384  etransclem23  37408  etransclem28  37413  etransclem32  37417  etransclem35  37420  etransclem48  37433  iccpartltu  37692  iccpartleu  37695  pgrple2abl  38469  difmodm1lt  38645  nnpw2blen  38711  dignn0flhalflem1  38746