Theorem eqbrtrd 4422

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

Syntax hints:   -> wi 4   = wceq 1443   class class class wbr 4401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402

This theorem is referenced by:  eqbrtrrd  4424  somin2  5234  en1b  7634  domunsncan  7669  fodomfi  7847  hartogslem1  8054  wemaplem2  8059  infdifsn  8159  carddomi2  8401  cdaun  8599  cda1dif  8603  mapcdaen  8611  cdaxpdom  8616  cdafi  8617  cdainf  8619  carden  8973  alephsuc3  9002  fpwwe2lem6  9057  fpwwe2lem7  9058  inar1  9197  rankcf  9199  lesub3d  10228  lbinfle  10560  lbinfmleOLD  10561  supadd  10572  supmul  10576  rpnnen1lem3  11289  divge1  11364  xrmin1  11469  xrmin2  11470  ifle  11487  qbtwnxr  11490  xltnegi  11506  xleadd1a  11536  xlt2add  11543  xlemul1a  11571  xov1plusxeqvd  11775  ubmelm1fzo  12004  flflp1  12040  ceim1l  12071  ceilm1lt  12072  ceille  12074  quoremz  12079  quoremnn0ALT  12081  modlt  12104  modeqmodmin  12156  seqf1olem1  12249  bernneq  12395  discr  12406  faclbnd2  12473  faclbnd4lem3  12477  hashun2  12559  hashfun  12606  ccatsymb  12724  ccatrn  12730  sqrlem6  13304  sqrlem7  13305  rddif  13396  amgm2  13425  icodiamlt  13490  climconst  13600  rlimconst  13601  serclim0  13634  rlimcn1  13645  mulcn2  13652  reccn2  13653  o1mul  13671  o1rlimmul  13675  iserex  13713  climlec2  13715  iserge0  13717  climcau  13727  caucvgrlem  13729  caucvgrlemOLD  13730  caucvgr  13734  iseraltlem2  13742  iseraltlem3  13743  iseralt  13744  fsumabs  13854  o1fsum  13866  iserabs  13868  climfsum  13873  isumless  13896  climcndslem2  13901  divrcnv  13903  flo1  13905  supcvg  13907  georeclim  13921  geomulcvg  13925  cvgrat  13932  mertenslem1  13933  prodfclim1  13942  fprodge1  14042  fprodle  14043  efcvgfsum  14133  eftlub  14156  eflegeo  14168  tanhlt1  14207  tanhbnd  14208  ef01bndlem  14231  sin01bnd  14232  cos01bnd  14233  cos01gt0  14238  ruclem2  14277  ruclem3  14278  ruclem9  14283  ruclem11  14285  ruclem12  14286  bitsfzolem  14400  bitsfzolemOLD  14401  bitsfzo  14402  bitsinv1lem  14408  sadcaddlem  14424  mulgcd  14507  eucalglt  14537  lcmledvds  14557  lcmslefacOLD  14579  lcmfledvds  14598  prmind2  14628  isprm5  14644  mulgcddvds  14654  coprmproddvdslem  14672  divdenle  14691  nonsq  14701  pythagtriplem4  14762  pclem  14781  pcpremul  14786  pczdvds  14805  pcprmpw2  14824  qexpz  14839  prmreclem4  14856  prmreclem5  14857  4sqlem10  14884  ramtub  14961  ramtubOLD  14962  ramub2  14964  prmodvdslcmf  14998  prmorlefacOLD  15011  prmordvdslcmfOLD  15012  prmgaplem8  15021  natpropd  15874  catciso  15995  p0le  16282  acsdomd  16420  qusgrp  16865  f1otrspeq  17081  pmtrfrn  17092  pmtrfconj  17100  symggen  17104  psgnunilem4  17131  oddvds2  17210  odcau  17249  pgpfi  17250  pgpssslw  17259  sylow3lem4  17275  efgred2  17396  frgp0  17403  odadd2  17480  oddvdssubg  17486  ablfac1c  17697  ablfac1eu  17699  pgpfaclem3  17709  isabvd  18041  abvsubtri  18056  mplsubrg  18657  coe1sfi  18799  cyggic  19136  mp2pm2mplem5  19827  en2top  19994  1stcrest  20461  2ndcrest  20462  hausmapdom  20508  ufilen  20938  xmetrtri2  21364  prdsxmetlem  21376  bl2in  21408  xblcntrps  21418  xblcntr  21419  ssblps  21430  ssbl  21431  blssps  21432  blss  21433  blcld  21513  methaus  21528  metustexhalf  21564  nrginvrcnlem  21686  nrginvrcn  21687  nmoi  21726  nmoiOLD  21742  nmo0  21749  nmoid  21756  blcvx  21809  reperflem  21829  reconnlem2  21838  metdcnlem  21847  metdscn  21866  metnrmlem3  21871  metdscnOLD  21881  metnrmlem3OLD  21886  mulc1cncf  21930  iccpnfhmeo  21966  cnheiborlem  21975  cnheibor  21976  lebnumii  21990  pcopt  22046  pcopt2  22047  pcoass  22048  nmoleub2lem  22121  nmoleub2lem3  22122  nmoleub2lem2  22123  ipcau2  22201  tchcphlem1  22202  trirn  22347  rrxdstprj1  22356  minveclem3  22364  minveclem3OLD  22376  ivthlem2  22396  ivthlem3  22397  ivth2  22399  ovollb  22425  ovolsslem  22430  ovollb2lem  22434  ovolctb  22436  ovoliunlem1  22448  ovolsca  22461  ovolicc1  22462  ovolicc2lem4OLD  22466  ovolicc2lem4  22467  nulmbl  22482  ioombl1lem4  22507  uniioovol  22529  uniioombllem3a  22535  uniioombllem4  22537  opnmbllem  22552  volcn  22557  volivth  22558  i1fadd  22646  i1fmul  22647  mbfi1fseqlem4  22669  mbfi1fseqlem5  22670  mbfi1fseqlem6  22671  itg2const2  22692  itg2seq  22693  itg2uba  22694  itg2split  22700  itg2monolem1  22701  itg2monolem3  22703  itg2i1fseq2  22707  itg2addlem  22709  itg2gt0  22711  itg2cnlem1  22712  itg2cnlem2  22713  itgless  22767  ibladdlem  22770  bddmulibl  22789  dveflem  22924  dvferm1lem  22929  dvferm2lem  22931  dvlip  22938  dvlipcn  22939  dvlip2  22940  dvle  22952  dvivthlem1  22953  lhop1lem  22958  dvcvx  22965  dvfsumabs  22968  dvfsumlem2  22972  dvfsumlem4  22974  dvfsumrlim2  22977  dvfsum2  22979  ftc1a  22982  ftc1lem4  22984  ftc1lem5  22985  deg1sub  23050  ply1divex  23080  deg1submon1p  23096  r1pdeglt  23102  dvdsq1p  23104  fta1glem2  23110  fta1g  23111  plyeq0lem  23157  dgrlt  23213  fta1lem  23253  aalioulem2  23282  aalioulem3  23283  aalioulem4  23284  aaliou3lem2  23292  aaliou3lem9  23299  taylply2  23316  ulmbdd  23346  ulmdvlem1  23348  mtest  23352  mtestbdd  23353  radcnvlem1  23361  radcnvle  23368  pserulm  23370  psercn  23374  pserdvlem2  23376  abelthlem2  23380  abelthlem5  23383  abelthlem7  23386  abelthlem8  23387  abelthlem9  23388  reeff1olem  23394  tangtx  23453  tanord  23480  efif1olem4  23487  logrnaddcl  23517  logcj  23548  logimul  23556  logneg2  23557  logdivlti  23562  divlogrlim  23573  logcnlem3  23582  logcnlem4  23583  efopn  23596  logtayllem  23597  logtayl  23598  cxpcn3lem  23680  cxpaddle  23685  abscxpbnd  23686  asinlem3  23790  asinneg  23805  asinsin  23811  atanlogaddlem  23832  atantan  23842  bndatandm  23848  atans2  23850  atantayl  23856  atantayl2  23857  atantayl3  23858  leibpi  23861  birthdaylem3  23872  rlimcnp  23884  efrlim  23888  cxplim  23890  cxp2lim  23895  cxploglim2  23897  divsqrtsumo1  23902  jensenlem2  23906  amgm  23909  logdifbnd  23912  harmonicbnd4  23929  fsumharmonic  23930  lgamgulmlem2  23948  lgamgulmlem3  23949  lgamgulmlem5  23951  lgambdd  23955  lgamcvg2  23973  ftalem1  23990  ftalem5  23994  ftalem5OLD  23996  basellem1  24000  basellem8  24007  ppip1le  24081  ppiltx  24097  sqff1o  24102  chtublem  24132  chpub  24141  logfaclbnd  24143  logfacrlim  24145  logexprlim  24146  mersenne  24148  bcmono  24198  bcmax  24199  bposlem2  24206  bposlem5  24209  lgslem3  24219  lgsquadlem1  24275  lgsquadlem2  24276  2sqblem  24298  chebbnd1  24303  chtppilimlem1  24304  chto1ub  24307  chpchtlim  24310  chpo1ubb  24312  rplogsumlem1  24315  rplogsumlem2  24316  rpvmasumlem  24318  dchrisumlem1  24320  dchrisumlem2  24321  dchrmusum2  24325  dchrvmasumlem2  24329  dchrvmasumlem3  24330  dchrvmasumiflem1  24332  dchrisum0flblem1  24339  dchrisum0fno1  24342  dchrisum0lem1b  24346  dchrisum0lem1  24347  dchrisum0lem2a  24348  dchrisum0lem2  24349  rplogsum  24358  mudivsum  24361  mulogsumlem  24362  mulog2sumlem1  24365  mulog2sumlem2  24366  vmalogdivsum2  24369  2vmadivsumlem  24371  selberglem2  24377  selberg2b  24383  logdivbnd  24387  selberg3lem1  24388  selberg3lem2  24389  selberg4lem1  24391  pntrmax  24395  pntrsumo1  24396  pntrlog2bndlem1  24408  pntrlog2bndlem2  24409  pntrlog2bndlem3  24410  pntrlog2bndlem4  24411  pntrlog2bndlem5  24412  pntrlog2bnd  24415  pntpbnd1a  24416  pntpbnd2  24418  pntibndlem2  24422  pntlemb  24428  pntlemg  24429  pntlemh  24430  pntlemr  24433  pntlemj  24434  pntlemf  24436  pntlemo  24438  pnt  24445  padicabv  24461  ostth2lem2  24465  ostth2lem3  24466  ostth3  24469  colperpexlem3  24767  mideulem2  24769  lnperpex  24838  trgcopy  24839  iscgra1  24845  brbtwn2  24928  colinearalglem4  24932  nvmtri2  26294  nvabs  26295  nvge0  26296  nvlmle  26321  smcnlem  26326  nmblolbii  26433  blocnilem  26438  siii  26487  ubthlem2  26506  minvecolem3  26511  minvecolem3OLD  26521  htthlem  26563  bcsiALT  26825  bcs3  26829  chscllem4  27286  0cnop  27625  0cnfn  27626  nmbdoplbi  27670  nmcoplbi  27674  nmophmi  27677  nmbdfnlbi  27695  nmcfnlbi  27698  nlelchi  27707  riesz1  27711  cnlnadjlem2  27714  nmopadjlei  27734  nmoptrii  27740  nmopcoi  27741  nmopcoadji  27747  unierri  27750  branmfn  27751  pjs14i  27856  hstle  27876  cdj3lem2b  28083  xlt2addrd  28331  eliccelico  28352  elicoelioo  28353  ltesubnnd  28378  archirngz  28499  archiabllem2c  28505  madjusmdetlem2  28647  locfinref  28661  sqsscirc1  28707  tpr2rico  28711  esumcst  28877  esumgect  28904  esum2d  28907  measunl  29031  measiun  29033  omssubaddlem  29120  omssubadd  29121  omssubaddOLD  29125  carsgsigalem  29140  carsgclctunlem2  29144  pmeasmono  29150  eulerpartlemgc  29188  eulerpartlemb  29194  ballotlemsel1i  29338  ballotlemro  29348  ballotlemsel1iOLD  29376  ballotlemroOLD  29386  sgnsub  29408  signsplypnf  29432  signsply0  29433  signsvtn  29466  signsvfnn  29468  erdsze2lem1  29919  sinccvglem  30309  divcnvlin  30360  iprodefisum  30370  faclimlem2  30373  nodense  30571  nobnddown  30583  fnemeet1  31015  ltflcei  31926  ptrecube  31933  poimirlem16  31949  poimirlem17  31950  poimirlem29  31962  broucube  31967  opnmbllem0  31969  mblfinlem2  31971  mblfinlem3  31972  ismblfin  31974  itg2addnclem  31986  itg2addnclem2  31987  itg2addnclem3  31988  itg2addnc  31989  ibladdnclem  31991  ftc1cnnclem  32008  ftc1cnnc  32009  ftc1anc  32018  geomcau  32081  prdsbnd  32118  cntotbnd  32121  heiborlem4  32139  rrndstprj2  32156  rrncmslem  32157  rrnequiv  32160  iccbnd  32165  cvlcvr1  32899  cvrat3  33001  dalem25  33257  cdlema1N  33350  dalawlem3  33432  dalawlem4  33433  dalawlem5  33434  dalawlem6  33435  dalawlem7  33436  dalawlem9  33438  dalawlem11  33440  dalawlem12  33441  lhp2lt  33560  lhpmcvr  33582  4atexlemcnd  33631  lautj  33652  trlle  33744  trlval3  33747  trlval4  33748  cdleme0moN  33785  cdleme13  33832  cdleme15  33838  cdleme19b  33865  cdleme20e  33874  cdleme20j  33879  cdleme22e  33905  cdleme22eALTN  33906  cdleme26fALTN  33923  cdleme26f  33924  cdleme27N  33930  cdleme41sn3a  33994  cdleme46fsvlpq  34066  cdlemeg46vrg  34088  cdlemg4  34178  cdlemg7N  34187  cdlemg9a  34193  cdlemg11b  34203  cdlemg12a  34204  trljco  34301  tendoidcl  34330  tendococl  34333  tendopltp  34341  tendo0tp  34350  tendoicl  34357  cdlemi2  34380  cdlemk5a  34396  cdlemk5  34397  cdlemk12  34411  cdlemkole  34414  cdlemk14  34415  cdlemk12u  34433  cdlemk37  34475  cdlemk39s-id  34501  cdlemk49  34512  cdlemk39u1  34528  cdlemk39u  34529  dian0  34601  cdlemm10N  34680  cdlemn2  34757  cdlemn10  34768  dihord1  34780  dihord10  34785  dihmeetlem4preN  34868  dihmeetlem18N  34886  dihmeetlem20N  34888  dihjatc  34979  mapdcnvatN  35228  lzenom  35606  irrapxlem2  35661  irrapxlem3  35662  irrapxlem5  35664  pellexlem2  35668  pell14qrgt0  35699  pellfundlb  35726  pellfundex  35728  pellfund14  35740  rmspecsqrtnq  35748  jm2.24nn  35803  jm2.17a  35804  jm2.17b  35805  congabseq  35818  acongrep  35824  acongeq  35827  jm2.26lem3  35850  jm2.27a  35854  jm2.27c  35856  hbtlem2  35977  dgraaub  36007  dgraaubOLD  36008  idomodle  36064  relexpxpmin  36303  frege102d  36340  hashnzfzclim  36665  binomcxplemfrat  36694  binomcxplemnotnn0  36699  suprnmpt  37433  mpct  37476  dstregt0  37485  lefldiveq  37500  fzisoeu  37512  upbdrech  37517  ssfiunibd  37521  fzdifsuc2  37524  xadd0ge  37536  supxrgere  37550  supxrge  37555  suplesup  37556  xrlexaddrp  37569  ioondisj2  37583  iccshift  37613  iooshift  37617  fmul01  37652  fmul01lt1lem1  37656  fmul01lt1lem2  37657  climrec  37675  climsuse  37681  mullimc  37690  mullimcf  37697  constlimc  37698  idlimc  37700  divcnvg  37701  limcperiod  37702  limcrecl  37703  lptioo2  37705  lptioo1  37706  islpcn  37713  lptre2pt  37714  limcleqr  37719  neglimc  37722  addlimc  37723  0ellimcdiv  37724  limclner  37726  sinaover2ne0  37737  cncfshift  37745  cncfperiod  37750  cncfioobdlem  37768  cncfioobd  37769  fperdvper  37784  dvdivbd  37789  dvbdfbdioolem1  37794  dvbdfbdioolem2  37795  ioodvbdlimc1lem1  37797  ioodvbdlimc1lem2  37798  ioodvbdlimc1lem1OLD  37799  ioodvbdlimc1lem2OLD  37800  ioodvbdlimc2lem  37802  ioodvbdlimc2lemOLD  37803  dvnmul  37812  dvnprodlem1  37815  itgiccshift  37851  itgperiod  37852  stoweidlem1  37855  stoweidlem11  37865  stoweidlem13  37867  stoweidlem14  37868  stoweidlem16  37870  stoweidlem21  37875  stoweidlem25  37879  stoweidlem26  37880  stoweidlem36  37891  stoweidlem38  37893  stoweidlem41  37896  stoweidlem42  37897  stoweidlem45  37900  stoweidlem48  37903  stoweidlem52  37907  stoweidlem62  37917  stoweidlem62OLD  37918  wallispilem3  37923  stirlinglem5  37934  stirlinglem6  37935  stirlinglem7  37936  stirlinglem10  37939  stirlinglem12  37941  stirlinglem15  37944  dirkercncflem1  37959  fourierdlem10  37973  fourierdlem12  37975  fourierdlem15  37978  fourierdlem16  37979  fourierdlem19  37982  fourierdlem20  37983  fourierdlem21  37984  fourierdlem22  37985  fourierdlem24  37987  fourierdlem30  37993  fourierdlem37  38001  fourierdlem39  38003  fourierdlem40  38004  fourierdlem41  38005  fourierdlem42  38006  fourierdlem42OLD  38007  fourierdlem47  38011  fourierdlem48  38012  fourierdlem49  38013  fourierdlem50  38014  fourierdlem52  38016  fourierdlem54  38018  fourierdlem60  38024  fourierdlem61  38025  fourierdlem63  38027  fourierdlem64  38028  fourierdlem68  38032  fourierdlem71  38035  fourierdlem72  38036  fourierdlem73  38037  fourierdlem74  38038  fourierdlem75  38039  fourierdlem76  38040  fourierdlem77  38041  fourierdlem78  38042  fourierdlem79  38043  fourierdlem81  38045  fourierdlem82  38046  fourierdlem83  38047  fourierdlem84  38048  fourierdlem87  38051  fourierdlem92  38056  fourierdlem93  38057  fourierdlem94  38058  fourierdlem101  38065  fourierdlem102  38066  fourierdlem103  38067  fourierdlem104  38068  fourierdlem111  38075  fourierdlem112  38076  fourierdlem113  38077  fourierdlem114  38078  sqwvfoura  38086  sqwvfourb  38087  fouriersw  38089  elaa2lem  38091  elaa2lemOLD  38092  etransclem23  38116  etransclem28  38121  etransclem32  38125  etransclem35  38128  etransclem48OLD  38141  etransclem48  38142  qndenserrnbllem  38157  salexct  38187  sge0fsum  38223  sge0supre  38225  sge0rnbnd  38229  sge0lefi  38234  sge0lessmpt  38235  sge0ltfirp  38236  sge0prle  38237  sge0resrnlem  38239  sge0le  38243  sge0split  38245  sge0iunmptlemre  38251  sge0iunmpt  38254  sge0isum  38263  sge0xaddlem1  38269  sge0xaddlem2  38270  sge0xadd  38271  meaunle  38296  meaiunlelem  38300  omeunle  38331  omeiunle  38332  omelesplit  38333  omeiunltfirp  38334  carageniuncllem2  38337  caratheodorylem2  38342  caragencmpl  38350  ovnlecvr  38374  ovncvrrp  38380  ovnsubaddlem1  38386  ovnsubadd  38388  hoidmv1lelem1  38407  hoidmv1lelem2  38408  hoidmv1le  38410  hoidmvlelem1  38411  hoidmvlelem2  38412  hoidmvlelem5  38415  hoidmvle  38416  ovnhoilem1  38417  ovnlecvr2  38426  ovncvr2  38427  hoiqssbllem2  38439  hspmbllem2  38443  hspmbllem3  38444  iccpartltu  38733  iccpartleu  38736  subupgr  39342  pgrple2abl  40137  difmodm1lt  40312  nnpw2blen  40378  dignn0flhalflem1  40413