Theorem eqbrtrd 4410

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

Syntax hints:   -> wi 4   = wceq 1370   class class class wbr 4390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-br 4391

This theorem is referenced by:  eqbrtrrd  4412  somin2  5334  en1b  7477  domunsncan  7511  fodomfi  7691  hartogslem1  7857  wemaplem2  7862  infdifsn  7963  carddomi2  8241  cdaun  8442  cda1dif  8446  mapcdaen  8454  cdaxpdom  8459  cdafi  8460  cdainf  8462  carden  8816  alephsuc3  8845  fpwwe2lem6  8903  fpwwe2lem7  8904  inar1  9043  rankcf  9045  lbinfmle  10386  supmul  10399  rpnnen1lem3  11082  xrmin1  11250  xrmin2  11251  ifle  11268  qbtwnxr  11271  xltnegi  11287  xleadd1a  11317  xlt2add  11324  xlemul1a  11352  xov1plusxeqvd  11532  ubmelm1fzo  11724  ceim1l  11787  ceilm1lt  11788  ceille  11790  quoremz  11795  quoremnn0ALT  11797  modlt  11819  modeqmodmin  11869  seqf1olem1  11946  bernneq  12091  discr  12102  faclbnd2  12168  faclbnd4lem3  12172  hashun2  12248  hashfun  12301  ccatsymb  12383  lswccat0lsw  12390  sqrlem6  12839  sqrlem7  12840  rddif  12930  amgm2  12959  climconst  13123  rlimconst  13124  serclim0  13157  rlimcn1  13168  mulcn2  13175  reccn2  13176  o1mul  13194  o1rlimmul  13198  iserex  13236  climlec2  13238  iserge0  13240  climcau  13250  caucvgrlem  13252  caucvgr  13255  iseraltlem2  13262  iseraltlem3  13263  iseralt  13264  fsumabs  13366  o1fsum  13378  iserabs  13380  climfsum  13385  isumless  13410  climcndslem2  13415  divrcnv  13417  flo1  13419  supcvg  13420  georeclim  13434  geomulcvg  13438  cvgrat  13445  mertenslem1  13446  efcvgfsum  13473  eftlub  13495  eflegeo  13507  tanhlt1  13546  tanhbnd  13547  ef01bndlem  13570  sin01bnd  13571  cos01bnd  13572  cos01gt0  13577  ruclem2  13616  ruclem3  13617  ruclem9  13622  ruclem11  13624  ruclem12  13625  bitsfzolem  13732  bitsfzo  13733  bitsinv1lem  13739  sadcaddlem  13755  mulgcd  13832  eucalglt  13862  prmind2  13876  mulgcddvds  13892  isprm5  13900  divdenle  13929  nonsq  13939  pythagtriplem4  13988  pclem  14007  pcpremul  14012  pczdvds  14031  pcprmpw2  14050  qexpz  14065  prmreclem4  14082  prmreclem5  14083  4sqlem10  14110  ramtub  14175  ramub2  14177  natpropd  14988  catciso  15077  p0le  15315  acsdomd  15453  divsgrp  15838  f1otrspeq  16055  pmtrfrn  16066  pmtrfconj  16074  symggen  16078  psgnunilem4  16105  oddvds2  16171  odcau  16207  pgpfi  16208  pgpssslw  16217  sylow3lem4  16233  efgred2  16354  frgp0  16361  odadd2  16435  oddvdssubg  16441  ablfac1c  16677  ablfac1eu  16679  pgpfaclem3  16689  isabvd  17011  abvsubtri  17026  mplsubrg  17626  coe1sfi  17775  cyggic  18114  en2top  18706  1stcrest  19173  2ndcrest  19174  hausmapdom  19220  ufilen  19619  xmetrtri2  20047  prdsxmetlem  20059  bl2in  20091  xblcntrps  20101  xblcntr  20102  ssblps  20113  ssbl  20114  blssps  20115  blss  20116  blcld  20196  methaus  20211  metustexhalfOLD  20254  metustexhalf  20255  nrginvrcnlem  20387  nrginvrcn  20388  nmoi  20423  nmo0  20430  nmoid  20437  blcvx  20491  reperflem  20511  reconnlem2  20520  metdcnlem  20529  metdscn  20548  metnrmlem3  20553  mulc1cncf  20597  iccpnfhmeo  20633  cnheiborlem  20642  cnheibor  20643  lebnumii  20654  pcopt  20710  pcopt2  20711  pcoass  20712  nmoleub2lem  20785  nmoleub2lem3  20786  nmoleub2lem2  20787  ipcau2  20865  tchcphlem1  20866  trirn  21015  rrxdstprj1  21024  minveclem3  21032  ivthlem2  21052  ivthlem3  21053  ivth2  21055  ovollb  21078  ovolsslem  21083  ovollb2lem  21087  ovolctb  21089  ovoliunlem1  21101  ovolsca  21114  ovolicc1  21115  ovolicc2lem4  21119  nulmbl  21133  ioombl1lem4  21158  uniioovol  21175  uniioombllem3a  21180  uniioombllem4  21182  opnmbllem  21197  volcn  21202  volivth  21203  i1fadd  21289  i1fmul  21290  mbfi1fseqlem4  21312  mbfi1fseqlem5  21313  mbfi1fseqlem6  21314  itg2const2  21335  itg2seq  21336  itg2uba  21337  itg2split  21343  itg2monolem1  21344  itg2monolem3  21346  itg2i1fseq2  21350  itg2addlem  21352  itg2gt0  21354  itg2cnlem1  21355  itg2cnlem2  21356  itgless  21410  ibladdlem  21413  bddmulibl  21432  dveflem  21567  dvferm1lem  21572  dvferm2lem  21574  dvlip  21581  dvlipcn  21582  dvlip2  21583  dvle  21595  dvivthlem1  21596  lhop1lem  21601  dvcvx  21608  dvfsumabs  21611  dvfsumlem2  21615  dvfsumlem4  21617  dvfsumrlim2  21620  dvfsum2  21622  ftc1a  21625  ftc1lem4  21627  ftc1lem5  21628  deg1sub  21696  ply1divex  21724  deg1submon1p  21740  r1pdeglt  21746  dvdsq1p  21748  fta1glem2  21754  fta1g  21755  plyeq0lem  21794  dgrlt  21849  fta1lem  21889  aalioulem2  21915  aalioulem3  21916  aalioulem4  21917  aaliou3lem2  21925  aaliou3lem9  21932  taylply2  21949  ulmbdd  21979  ulmdvlem1  21981  mtest  21985  mtestbdd  21986  radcnvlem1  21994  radcnvle  22001  pserulm  22003  psercn  22007  pserdvlem2  22009  abelthlem2  22013  abelthlem5  22016  abelthlem7  22019  abelthlem8  22020  abelthlem9  22021  reeff1olem  22027  tangtx  22083  tanord  22110  efif1olem4  22117  logrnaddcl  22142  logcj  22171  logimul  22179  logneg2  22180  logdivlti  22185  divlogrlim  22196  logcnlem3  22205  logcnlem4  22206  efopn  22219  logtayllem  22220  logtayl  22221  cxpcn3lem  22301  cxpaddle  22306  abscxpbnd  22307  asinlem3  22382  asinneg  22397  asinsin  22403  atanlogaddlem  22424  atantan  22434  bndatandm  22440  atans2  22442  atantayl  22448  atantayl2  22449  atantayl3  22450  leibpi  22453  birthdaylem3  22463  rlimcnp  22475  efrlim  22479  cxplim  22481  cxp2lim  22486  cxploglim2  22488  divsqrsumo1  22493  jensenlem2  22497  amgm  22500  logdifbnd  22503  harmonicbnd4  22520  fsumharmonic  22521  ftalem1  22526  ftalem5  22530  basellem1  22534  basellem8  22541  ppip1le  22615  ppiltx  22631  sqff1o  22636  chtublem  22666  chpub  22675  logfaclbnd  22677  logfacrlim  22679  logexprlim  22680  mersenne  22682  bcmono  22732  bcmax  22733  bposlem2  22740  bposlem5  22743  lgslem3  22753  lgsquadlem1  22809  lgsquadlem2  22810  2sqblem  22832  chebbnd1  22837  chtppilimlem1  22838  chto1ub  22841  chpchtlim  22844  chpo1ubb  22846  rplogsumlem1  22849  rplogsumlem2  22850  rpvmasumlem  22852  dchrisumlem1  22854  dchrisumlem2  22855  dchrmusum2  22859  dchrvmasumlem2  22863  dchrvmasumlem3  22864  dchrvmasumiflem1  22866  dchrisum0flblem1  22873  dchrisum0fno1  22876  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem2  22883  rplogsum  22892  mudivsum  22895  mulogsumlem  22896  mulog2sumlem1  22899  mulog2sumlem2  22900  vmalogdivsum2  22903  2vmadivsumlem  22905  selberglem2  22911  selberg2b  22917  logdivbnd  22921  selberg3lem1  22922  selberg3lem2  22923  selberg4lem1  22925  pntrmax  22929  pntrsumo1  22930  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bnd  22949  pntpbnd1a  22950  pntpbnd2  22952  pntibndlem2  22956  pntlemb  22962  pntlemg  22963  pntlemh  22964  pntlemr  22967  pntlemj  22968  pntlemf  22970  pntlemo  22972  pnt  22979  padicabv  22995  ostth2lem2  22999  ostth2lem3  23000  ostth3  23003  colperplem3  23242  mideulem  23244  brbtwn2  23286  colinearalglem4  23290  nvmtri2  24195  nvabs  24196  nvge0  24197  nvlmle  24222  smcnlem  24227  nmblolbii  24334  blocnilem  24339  siii  24388  ubthlem2  24407  minvecolem3  24412  htthlem  24454  bcsiALT  24716  bcs3  24720  chscllem4  25178  0cnop  25518  0cnfn  25519  nmbdoplbi  25563  nmcoplbi  25567  nmophmi  25570  nmbdfnlbi  25588  nmcfnlbi  25591  nlelchi  25600  riesz1  25604  cnlnadjlem2  25607  nmopadjlei  25627  nmoptrii  25633  nmopcoi  25634  nmopcoadji  25640  unierri  25643  branmfn  25644  pjs14i  25749  hstle  25769  cdj3lem2b  25976  xlt2addrd  26185  eliccelico  26201  elicoelioo  26202  ltesubnnd  26225  archirngz  26340  archiabllem2c  26346  sqsscirc1  26472  tpr2rico  26476  esumcst  26648  measunl  26764  measiun  26766  eulerpartlemgc  26879  eulerpartlemb  26885  ballotlemsel1i  27029  ballotlemro  27039  sgnsub  27061  signsplypnf  27085  signsply0  27086  signsvtn  27119  signsvfnn  27121  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem5  27153  lgambdd  27157  lgamcvg2  27175  erdsze2lem1  27225  sinccvglem  27451  divcnvlin  27533  prodfclim1  27542  iprodefisum  27639  faclimlem2  27684  nodense  27964  nobnddown  27976  supadd  28556  ltflcei  28557  lxflflp1  28559  opnmbllem0  28565  mblfinlem2  28567  mblfinlem3  28568  ismblfin  28570  itg2addnclem  28581  itg2addnclem2  28582  itg2addnclem3  28583  itg2addnc  28584  ibladdnclem  28586  ftc1cnnclem  28603  ftc1cnnc  28604  ftc1anc  28613  fnemeet1  28725  geomcau  28793  prdsbnd  28830  cntotbnd  28833  heiborlem4  28851  rrndstprj2  28868  rrncmslem  28869  rrnequiv  28872  iccbnd  28877  lzenom  29246  icodiamlt  29299  irrapxlem2  29302  irrapxlem3  29303  irrapxlem5  29305  pellexlem2  29309  pell14qrgt0  29338  pellfundlb  29363  pellfundex  29365  pellfund14  29377  rmspecsqrnq  29385  jm2.24nn  29440  jm2.17a  29441  jm2.17b  29442  congabseq  29455  acongrep  29461  acongeq  29464  jm2.26lem3  29488  jm2.27a  29492  jm2.27c  29494  hbtlem2  29618  dgraaub  29643  idomodle  29699  fmul01  29899  fmul01lt1lem1  29903  fmul01lt1lem2  29904  climrec  29914  climsuse  29919  stoweidlem1  29934  stoweidlem11  29944  stoweidlem13  29946  stoweidlem14  29947  stoweidlem16  29949  stoweidlem21  29954  stoweidlem25  29958  stoweidlem26  29959  stoweidlem36  29969  stoweidlem38  29971  stoweidlem41  29974  stoweidlem42  29975  stoweidlem45  29978  stoweidlem48  29981  stoweidlem52  29985  stoweidlem62  29995  wallispilem3  30000  stirlinglem5  30011  stirlinglem6  30012  stirlinglem7  30013  stirlinglem10  30016  stirlinglem12  30018  stirlinglem15  30021  elfzom1elfzo  30355  pgrple2abel  30908  mp2pm2mplem5  31265  cvlcvr1  33290  cvrat3  33392  dalem25  33648  cdlema1N  33741  dalawlem3  33823  dalawlem4  33824  dalawlem5  33825  dalawlem6  33826  dalawlem7  33827  dalawlem9  33829  dalawlem11  33831  dalawlem12  33832  lhp2lt  33951  lhpmcvr  33973  4atexlemcnd  34022  lautj  34043  trlle  34134  trlval3  34137  trlval4  34138  cdleme0moN  34175  cdleme13  34222  cdleme15  34228  cdleme19b  34254  cdleme20e  34263  cdleme20j  34268  cdleme22e  34294  cdleme22eALTN  34295  cdleme26fALTN  34312  cdleme26f  34313  cdleme27N  34319  cdleme41sn3a  34383  cdleme46fsvlpq  34455  cdlemeg46vrg  34477  cdlemg4  34567  cdlemg7N  34576  cdlemg9a  34582  cdlemg11b  34592  cdlemg12a  34593  trljco  34690  tendoidcl  34719  tendococl  34722  tendopltp  34730  tendo0tp  34739  tendoicl  34746  cdlemi2  34769  cdlemk5a  34785  cdlemk5  34786  cdlemk12  34800  cdlemkole  34803  cdlemk14  34804  cdlemk12u  34822  cdlemk37  34864  cdlemk39s-id  34890  cdlemk49  34901  cdlemk39u1  34917  cdlemk39u  34918  dian0  34990  cdlemm10N  35069  cdlemn2  35146  cdlemn10  35157  dihord1  35169  dihord10  35174  dihmeetlem4preN  35257  dihmeetlem18N  35275  dihmeetlem20N  35277  dihjatc  35368  mapdcnvatN  35617