Theorem eqbrtrd 4192

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

Syntax hints:   -> wi 4   = wceq 1649   class class class wbr 4172

This theorem is referenced by:  eqbrtrrd  4194  somin2  5231  en1b  7134  domunsncan  7167  fodomfi  7344  hartogslem1  7467  wemaplem2  7472  infdifsn  7567  carddomi2  7813  cdaun  8008  cda1dif  8012  mapcdaen  8020  cdaxpdom  8025  cdafi  8026  cdainf  8028  carden  8382  alephsuc3  8411  fpwwe2lem6  8466  fpwwe2lem7  8467  inar1  8606  rankcf  8608  lbinfmle  9919  supmul  9932  rpnnen1lem3  10558  xrmin1  10721  xrmin2  10722  ifle  10739  qbtwnxr  10742  xltnegi  10758  xleadd1a  10788  xlt2add  10795  xlemul1a  10823  xov1plusxeqvd  10997  ceim1l  11189  quoremz  11191  quoremnn0ALT  11193  modlt  11213  seqf1olem1  11317  bernneq  11460  discr  11471  faclbnd2  11537  faclbnd4lem3  11541  hashun2  11612  hashfun  11655  sqrlem6  12008  sqrlem7  12009  rddif  12099  amgm2  12128  climconst  12292  rlimconst  12293  serclim0  12326  rlimcn1  12337  mulcn2  12344  reccn2  12345  o1mul  12363  o1rlimmul  12367  iserex  12405  climlec2  12407  iserge0  12409  climcau  12419  caucvgrlem  12421  caucvgr  12424  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  fsumabs  12535  o1fsum  12547  iserabs  12549  climfsum  12554  isumless  12580  climcndslem2  12585  divrcnv  12587  flo1  12589  supcvg  12590  georeclim  12604  geomulcvg  12608  cvgrat  12615  mertenslem1  12616  efcvgfsum  12643  eftlub  12665  eflegeo  12677  tanhlt1  12716  tanhbnd  12717  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  cos01gt0  12747  ruclem2  12786  ruclem3  12787  ruclem9  12792  ruclem11  12794  ruclem12  12795  bitsfzolem  12901  bitsfzo  12902  bitsinv1lem  12908  sadcaddlem  12924  mulgcd  13001  eucalglt  13031  prmind2  13045  mulgcddvds  13059  isprm5  13067  divdenle  13096  nonsq  13106  pythagtriplem4  13148  pclem  13167  pcpremul  13172  pczdvds  13191  pcprmpw2  13210  qexpz  13225  prmreclem4  13242  prmreclem5  13243  4sqlem10  13270  ramtub  13335  ramub2  13337  natpropd  14128  catciso  14217  p0le  14427  acsdomd  14562  divsgrp  14950  oddvds2  15157  odcau  15193  pgpfi  15194  pgpssslw  15203  sylow3lem4  15219  efgred2  15340  frgp0  15347  odadd2  15419  oddvdssubg  15425  ablfac1c  15584  ablfac1eu  15586  pgpfaclem3  15596  isabvd  15863  abvsubtri  15878  cyggic  16808  en2top  17005  1stcrest  17469  2ndcrest  17470  hausmapdom  17516  ufilen  17915  xmetrtri2  18339  prdsxmetlem  18351  bl2in  18383  xblcntrps  18393  xblcntr  18394  ssblps  18405  ssbl  18406  blssps  18407  blss  18408  blcld  18488  methaus  18503  metustexhalfOLD  18546  metustexhalf  18547  nrginvrcnlem  18679  nrginvrcn  18680  nmoi  18715  nmo0  18722  nmoid  18729  blcvx  18782  reperflem  18802  reconnlem2  18811  metdcnlem  18820  metdscn  18839  metnrmlem3  18844  mulc1cncf  18888  iccpnfhmeo  18923  cnheiborlem  18932  cnheibor  18933  lebnumii  18944  pcopt  19000  pcopt2  19001  pcoass  19002  nmoleub2lem  19075  nmoleub2lem3  19076  nmoleub2lem2  19077  ipcau2  19144  tchcphlem1  19145  minveclem3  19283  ivthlem2  19302  ivthlem3  19303  ivth2  19305  ovollb  19328  ovolsslem  19333  ovollb2lem  19337  ovolctb  19339  ovoliunlem1  19351  ovolsca  19364  ovolicc1  19365  ovolicc2lem4  19369  nulmbl  19383  ioombl1lem4  19408  uniioovol  19424  uniioombllem3a  19429  uniioombllem4  19431  opnmbllem  19446  volcn  19451  volivth  19452  i1fadd  19540  i1fmul  19541  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  itg2const2  19586  itg2seq  19587  itg2uba  19588  itg2split  19594  itg2monolem1  19595  itg2monolem3  19597  itg2i1fseq2  19601  itg2addlem  19603  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  itgless  19661  ibladdlem  19664  bddmulibl  19683  dveflem  19816  dvferm1lem  19821  dvferm2lem  19823  dvlip  19830  dvlipcn  19831  dvlip2  19832  dvle  19844  dvivthlem1  19845  lhop1lem  19850  dvcvx  19857  dvfsumabs  19860  dvfsumlem2  19864  dvfsumlem4  19866  dvfsumrlim2  19869  dvfsum2  19871  ftc1a  19874  ftc1lem4  19876  ftc1lem5  19877  deg1sub  19984  ply1divex  20012  deg1submon1p  20028  r1pdeglt  20034  dvdsq1p  20036  fta1glem2  20042  fta1g  20043  plyeq0lem  20082  dgrlt  20137  fta1lem  20177  aalioulem2  20203  aalioulem3  20204  aalioulem4  20205  aaliou3lem2  20213  aaliou3lem9  20220  taylply2  20237  ulmbdd  20267  ulmdvlem1  20269  mtest  20273  mtestbdd  20274  radcnvlem1  20282  radcnvle  20289  pserulm  20291  psercn  20295  pserdvlem2  20297  abelthlem2  20301  abelthlem5  20304  abelthlem7  20307  abelthlem8  20308  abelthlem9  20309  reeff1olem  20315  tangtx  20366  tanord  20393  efif1olem4  20400  logrnaddcl  20425  logcj  20454  logimul  20462  logneg2  20463  logdivlti  20468  divlogrlim  20479  logcnlem3  20488  logcnlem4  20489  efopn  20502  logtayllem  20503  logtayl  20504  cxpcn3lem  20584  cxpaddle  20589  abscxpbnd  20590  asinlem3  20664  asinneg  20679  asinsin  20685  atanlogaddlem  20706  atantan  20716  bndatandm  20722  atans2  20724  atantayl  20730  atantayl2  20731  atantayl3  20732  leibpi  20735  birthdaylem3  20745  rlimcnp  20757  efrlim  20761  cxplim  20763  cxp2lim  20768  cxploglim2  20770  divsqrsumo1  20775  jensenlem2  20779  amgm  20782  logdifbnd  20785  harmonicbnd4  20802  fsumharmonic  20803  ftalem1  20808  ftalem5  20812  basellem1  20816  basellem8  20823  ppip1le  20897  ppiltx  20913  sqff1o  20918  chtublem  20948  chpub  20957  logfaclbnd  20959  logfacrlim  20961  logexprlim  20962  mersenne  20964  bcmono  21014  bcmax  21015  bposlem2  21022  bposlem5  21025  lgslem3  21035  lgsquadlem1  21091  lgsquadlem2  21092  2sqblem  21114  chebbnd1  21119  chtppilimlem1  21120  chto1ub  21123  chpchtlim  21126  chpo1ubb  21128  rplogsumlem1  21131  rplogsumlem2  21132  rpvmasumlem  21134  dchrisumlem1  21136  dchrisumlem2  21137  dchrmusum2  21141  dchrvmasumlem2  21145  dchrvmasumlem3  21146  dchrvmasumiflem1  21148  dchrisum0flblem1  21155  dchrisum0fno1  21158  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  rplogsum  21174  mudivsum  21177  mulogsumlem  21178  mulog2sumlem1  21181  mulog2sumlem2  21182  vmalogdivsum2  21185  2vmadivsumlem  21187  selberglem2  21193  selberg2b  21199  logdivbnd  21203  selberg3lem1  21204  selberg3lem2  21205  selberg4lem1  21207  pntrmax  21211  pntrsumo1  21212  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bnd  21231  pntpbnd1a  21232  pntpbnd2  21234  pntibndlem2  21238  pntlemb  21244  pntlemg  21245  pntlemh  21246  pntlemr  21249  pntlemj  21250  pntlemf  21252  pntlemo  21254  pnt  21261  padicabv  21277  ostth2lem2  21281  ostth2lem3  21282  ostth3  21285  nvmtri2  22114  nvabs  22115  nvge0  22116  nvlmle  22141  smcnlem  22146  nmblolbii  22253  blocnilem  22258  siii  22307  ubthlem2  22326  minvecolem3  22331  htthlem  22373  bcsiALT  22634  bcs3  22638  chscllem4  23095  0cnop  23435  0cnfn  23436  nmbdoplbi  23480  nmcoplbi  23484  nmophmi  23487  nmbdfnlbi  23505  nmcfnlbi  23508  nlelchi  23517  riesz1  23521  cnlnadjlem2  23524  nmopadjlei  23544  nmoptrii  23550  nmopcoi  23551  nmopcoadji  23557  unierri  23560  branmfn  23561  pjs14i  23666  hstle  23686  cdj3lem2b  23893  xlt2addrd  24077  eliccelico  24093  elicoelioo  24094  ltesubnnd  24115  sqsscirc1  24259  tpr2rico  24263  esumcst  24408  measunl  24523  measiun  24525  ballotlemsel1i  24723  ballotlemro  24733  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem5  24770  lgambdd  24774  lgamcvg2  24792  erdsze2lem1  24842  sinccvglem  25062  divcnvlin  25165  prodfclim1  25174  iprodefisum  25271  faclimlem2  25311  nodense  25557  nobnddown  25569  brbtwn2  25748  colinearalglem4  25752  supadd  26138  ltflcei  26140  lxflflp1  26142  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  ibladdnclem  26160  ftc1cnnclem  26177  ftc1cnnc  26178  fnemeet1  26285  trirn  26347  geomcau  26355  prdsbnd  26392  cntotbnd  26395  heiborlem4  26413  rrndstprj2  26430  rrncmslem  26431  rrnequiv  26434  iccbnd  26439  lzenom  26718  icodiamlt  26773  irrapxlem2  26776  irrapxlem3  26777  irrapxlem5  26779  pellexlem2  26783  pell14qrgt0  26812  pellfundlb  26837  pellfundex  26839  pellfund14  26851  rmspecsqrnq  26859  jm2.24nn  26914  jm2.17a  26915  jm2.17b  26916  congabseq  26929  acongrep  26935  acongeq  26938  jm2.26lem3  26962  jm2.27a  26966  jm2.27c  26968  hbtlem2  27196  dgraaub  27221  f1otrspeq  27258  pmtrfrn  27268  pmtrfconj  27275  symggen  27279  psgnunilem4  27288  idomodle  27380  fmul01  27577  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climrec  27596  climsuse  27601  stoweidlem1  27617  stoweidlem11  27627  stoweidlem13  27629  stoweidlem14  27630  stoweidlem16  27632  stoweidlem21  27637  stoweidlem25  27641  stoweidlem26  27642  stoweidlem36  27652  stoweidlem38  27654  stoweidlem41  27657  stoweidlem42  27658  stoweidlem45  27661  stoweidlem48  27664  stoweidlem52  27668  stoweidlem62  27678  wallispilem3  27683  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem10  27699  stirlinglem12  27701  stirlinglem15  27704  cvlcvr1  29822  cvrat3  29924  dalem25  30180  cdlema1N  30273  dalawlem3  30355  dalawlem4  30356  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem9  30361  dalawlem11  30363  dalawlem12  30364  lhp2lt  30483  lhpmcvr  30505  4atexlemcnd  30554  lautj  30575  trlle  30666  trlval3  30669  trlval4  30670  cdleme0moN  30707  cdleme13  30754  cdleme15  30760  cdleme19b  30786  cdleme20e  30795  cdleme20j  30800  cdleme22e  30826  cdleme22eALTN  30827  cdleme26fALTN  30844  cdleme26f  30845  cdleme27N  30851  cdleme41sn3a  30915  cdleme46fsvlpq  30987  cdlemeg46vrg  31009  cdlemg4  31099  cdlemg7N  31108  cdlemg9a  31114  cdlemg11b  31124  cdlemg12a  31125  trljco  31222  tendoidcl  31251  tendococl  31254  tendopltp  31262  tendo0tp  31271  tendoicl  31278  cdlemi2  31301  cdlemk5a  31317  cdlemk5  31318  cdlemk12  31332  cdlemkole  31335  cdlemk14  31336  cdlemk12u  31354  cdlemk37  31396  cdlemk39s-id  31422  cdlemk49  31433  cdlemk39u1  31449  cdlemk39u  31450  dian0  31522  cdlemm10N  31601  cdlemn2  31678  cdlemn10  31689  dihord1  31701  dihord10  31706  dihmeetlem4preN  31789  dihmeetlem18N  31807  dihmeetlem20N  31809  dihjatc  31900  mapdcnvatN  32149

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173