Theorem eqbrtrd 5088

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqbrtrd.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
eqbrtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 5076	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 259	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  eqbrtrrd  5090  somin2  5995  en1b  8577  domunsncan  8617  fodomfi  8797  infsupprpr  8968  hartogslem1  9006  wemaplem2  9011  infdifsn  9120  carddomi2  9399  djuinf  9614  carden  9973  alephsuc3  10002  fpwwe2lem6  10057  fpwwe2lem7  10058  inar1  10197  rankcf  10199  lesub3d  11258  lbinfle  11596  supadd  11609  supmul  11613  rpnnen1lem3  12379  divge1  12458  xrmin1  12571  xrmin2  12572  ifle  12591  qbtwnxr  12594  xltnegi  12610  xleadd1a  12647  xlt2add  12654  xlemul1a  12682  xov1plusxeqvd  12885  ubmelm1fzo  13134  flflp1  13178  ceim1l  13216  ceilm1lt  13217  ceille  13219  quoremz  13224  quoremnn0ALT  13226  modlt  13249  modeqmodmin  13310  addmodlteq  13315  seqf1olem1  13410  bernneq  13591  discr  13602  faclbnd2  13652  faclbnd4lem3  13656  hashun2  13745  hashfun  13799  ccatsymb  13936  ccatrn  13943  sqrlem6  14607  sqrlem7  14608  rddif  14700  amgm2  14729  icodiamlt  14795  climconst  14900  rlimconst  14901  serclim0  14934  rlimcn1  14945  mulcn2  14952  reccn2  14953  o1mul  14971  o1rlimmul  14975  iserex  15013  climlec2  15015  iserge0  15017  climcau  15027  caucvgrlem  15029  caucvgr  15032  iseraltlem2  15039  iseraltlem3  15040  iseralt  15041  fsumabs  15156  o1fsum  15168  iserabs  15170  climfsum  15175  isumless  15200  climcndslem2  15205  divrcnv  15207  flo1  15209  supcvg  15211  georeclim  15228  geomulcvg  15232  cvgrat  15239  mertenslem1  15240  prodfclim1  15249  fprodle  15350  efcvgfsum  15439  eftlub  15462  eflegeo  15474  tanhlt1  15513  tanhbnd  15514  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  cos01gt0  15544  ruclem2  15585  ruclem3  15586  ruclem9  15591  ruclem11  15593  ruclem12  15594  bitsfzolem  15783  bitsfzo  15784  bitsinv1lem  15790  sadcaddlem  15806  mulgcd  15896  eucalglt  15929  lcmledvds  15943  lcmfledvds  15976  mulgcddvds  15999  coprmproddvdslem  16006  prmind2  16029  isprm5  16051  divdenle  16089  nonsq  16099  pythagtriplem4  16156  pclem  16175  pcpremul  16180  pczdvds  16199  pcprmpw2  16218  qexpz  16237  prmreclem4  16255  prmreclem5  16256  4sqlem10  16283  ramtub  16348  ramub2  16350  prmodvdslcmf  16383  prmgaplem8  16394  natpropd  17246  catciso  17367  p0le  17653  acsdomd  17791  triv1nsgd  18325  qusgrp  18335  f1otrspeq  18575  pmtrfrn  18586  pmtrfconj  18594  symggen  18598  psgnunilem4  18625  oddvds2  18693  odcau  18729  pgpfi  18730  pgpssslw  18739  sylow3lem4  18755  efgred2  18879  frgp0  18886  odadd2  18969  oddvdssubg  18975  ablfac1c  19193  ablfac1eu  19195  pgpfaclem3  19205  2nsgsimpgd  19224  isabvd  19591  abvsubtri  19606  mplsubrg  20220  coe1sfi  20381  cyggic  20719  mp2pm2mplem5  21418  en2top  21593  1stcrest  22061  2ndcrest  22062  hausmapdom  22108  ufilen  22538  xmetrtri2  22966  prdsxmetlem  22978  bl2in  23010  xblcntrps  23020  xblcntr  23021  ssblps  23032  ssbl  23033  blssps  23034  blss  23035  blcld  23115  methaus  23130  metustexhalf  23166  nmtri2  23236  tngngp3  23265  nrginvrcnlem  23300  nrginvrcn  23301  nmoi  23337  nmo0  23344  nmoid  23351  blcvx  23406  reperflem  23426  reconnlem2  23435  metdcnlem  23444  metdscn  23464  metnrmlem3  23469  mulc1cncf  23513  iccpnfhmeo  23549  cnheiborlem  23558  cnheibor  23559  lebnumii  23570  pcopt  23626  pcopt2  23627  pcoass  23628  nmoleub2lem  23718  nmoleub2lem3  23719  nmoleub2lem2  23720  ipcau2  23837  tcphcphlem1  23838  nglmle  23905  trirn  24003  rrxdstprj1  24012  minveclem3  24032  ivthlem2  24053  ivthlem3  24054  ivth2  24056  ovollb  24080  ovolsslem  24085  ovollb2lem  24089  ovolctb  24091  ovoliunlem1  24103  ovolsca  24116  ovolicc1  24117  ovolicc2lem4  24121  nulmbl  24136  ioombl1lem4  24162  uniioovol  24180  uniioombllem3a  24185  uniioombllem4  24187  opnmbllem  24202  volcn  24207  volivth  24208  i1fadd  24296  i1fmul  24297  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  itg2const2  24342  itg2seq  24343  itg2uba  24344  itg2split  24350  itg2monolem1  24351  itg2monolem3  24353  itg2i1fseq2  24357  itg2addlem  24359  itg2gt0  24361  itg2cnlem1  24362  itg2cnlem2  24363  itgless  24417  ibladdlem  24420  bddmulibl  24439  dveflem  24576  dvferm1lem  24581  dvferm2lem  24583  dvlip  24590  dvlipcn  24591  dvlip2  24592  dvle  24604  dvivthlem1  24605  lhop1lem  24610  dvcvx  24617  dvfsumabs  24620  dvfsumlem2  24624  dvfsumlem4  24626  dvfsumrlim2  24629  dvfsum2  24631  ftc1a  24634  ftc1lem4  24636  ftc1lem5  24637  deg1sub  24702  ply1divex  24730  deg1submon1p  24746  r1pdeglt  24752  dvdsq1p  24754  fta1glem2  24760  fta1g  24761  plyeq0lem  24800  dgrlt  24856  fta1lem  24896  aalioulem2  24922  aalioulem3  24923  aalioulem4  24924  aaliou3lem2  24932  aaliou3lem9  24939  taylply2  24956  ulmbdd  24986  ulmdvlem1  24988  mtest  24992  mtestbdd  24993  radcnvlem1  25001  radcnvle  25008  pserulm  25010  psercn  25014  pserdvlem2  25016  abelthlem2  25020  abelthlem5  25023  abelthlem7  25026  abelthlem8  25027  abelthlem9  25028  reeff1olem  25034  tangtx  25091  tanord  25122  efif1olem4  25129  logrnaddcl  25158  logcj  25189  logimul  25197  logneg2  25198  logdivlti  25203  divlogrlim  25218  logcnlem3  25227  logcnlem4  25228  efopn  25241  logtayllem  25242  logtayl  25243  cxpcn3lem  25328  cxpaddle  25333  abscxpbnd  25334  asinlem3  25449  asinneg  25464  asinsin  25470  atanlogaddlem  25491  atantan  25501  bndatandm  25507  atans2  25509  atantayl  25515  atantayl2  25516  atantayl3  25517  leibpi  25520  birthdaylem3  25531  rlimcnp  25543  efrlim  25547  cxplim  25549  cxp2lim  25554  cxploglim2  25556  divsqrtsumo1  25561  jensenlem2  25565  amgm  25568  logdifbnd  25571  harmonicbnd4  25588  fsumharmonic  25589  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem5  25610  lgambdd  25614  lgamcvg2  25632  ftalem1  25650  ftalem5  25654  basellem1  25658  basellem8  25665  ppip1le  25738  ppiltx  25754  sqff1o  25759  chtublem  25787  chpub  25796  logfaclbnd  25798  logfacrlim  25800  logexprlim  25801  mersenne  25803  bcmono  25853  bcmax  25854  bposlem2  25861  bposlem5  25864  lgslem3  25875  gausslemma2dlem1a  25941  lgsquadlem1  25956  lgsquadlem2  25957  2lgslem1c  25969  2sqblem  26007  chebbnd1  26048  chtppilimlem1  26049  chto1ub  26052  chpchtlim  26055  chpo1ubb  26057  rplogsumlem1  26060  rplogsumlem2  26061  rpvmasumlem  26063  dchrisumlem1  26065  dchrisumlem2  26066  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrvmasumiflem1  26077  dchrisum0flblem1  26084  dchrisum0fno1  26087  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  rplogsum  26103  mudivsum  26106  mulogsumlem  26107  mulog2sumlem1  26110  mulog2sumlem2  26111  vmalogdivsum2  26114  2vmadivsumlem  26116  selberglem2  26122  selberg2b  26128  logdivbnd  26132  selberg3lem1  26133  selberg3lem2  26134  selberg4lem1  26136  pntrmax  26140  pntrsumo1  26141  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem2  26167  pntlemb  26173  pntlemg  26174  pntlemh  26175  pntlemr  26178  pntlemj  26179  pntlemf  26181  pntlemo  26183  pnt  26190  padicabv  26206  ostth2lem2  26210  ostth2lem3  26211  ostth3  26214  colperpexlem3  26518  mideulem2  26520  lnperpex  26589  trgcopy  26590  iscgra1  26596  brbtwn2  26691  colinearalglem4  26695  subupgr  27069  crctcshwlkn0lem1  27588  nvabs  28449  nvge0  28450  smcnlem  28474  nmblolbii  28576  blocnilem  28581  siii  28630  ubthlem2  28648  minvecolem3  28653  htthlem  28694  bcsiALT  28956  bcs3  28960  chscllem4  29417  0cnop  29756  0cnfn  29757  nmbdoplbi  29801  nmcoplbi  29805  nmophmi  29808  nmbdfnlbi  29826  nmcfnlbi  29829  nlelchi  29838  riesz1  29842  cnlnadjlem2  29845  nmopadjlei  29865  nmoptrii  29871  nmopcoi  29872  nmopcoadji  29878  unierri  29881  branmfn  29882  pjs14i  29987  hstle  30007  cdj3lem2b  30214  xlt2addrd  30482  eliccelico  30500  elicoelioo  30501  ltesubnnd  30538  wrdt2ind  30627  archirngz  30818  archiabllem2c  30824  madjusmdetlem2  31093  locfinref  31105  sqsscirc1  31151  tpr2rico  31155  esumcst  31322  esumgect  31349  esum2d  31352  measunl  31475  measiun  31477  omssubaddlem  31557  omssubadd  31558  carsgsigalem  31573  carsgclctunlem2  31577  pmeasmono  31582  eulerpartlemgc  31620  eulerpartlemb  31626  ballotlemsel1i  31770  ballotlemro  31780  sgnsub  31802  signsplypnf  31820  signsply0  31821  signsvtn  31854  signsvfnn  31856  hgt750lemd  31919  logdivsqrle  31921  hashf1dmcdm  32356  erdsze2lem1  32450  sinccvglem  32915  divcnvlin  32964  iprodefisum  32973  faclimlem2  32976  nosep1o  33186  nodense  33196  fnemeet1  33714  dnibndlem10  33826  dnibndlem11  33827  dnibnd  33830  knoppcnlem4  33835  knoppcnlem6  33837  unblimceq0lem  33845  unbdqndv2lem1  33848  unbdqndv2lem2  33849  knoppndvlem11  33861  knoppndvlem12  33862  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem18  33868  knoppndvlem19  33869  knoppndvlem21  33871  ctbssinf  34690  ltflcei  34895  ptrecube  34907  poimirlem16  34923  poimirlem17  34924  poimirlem29  34936  broucube  34941  opnmbllem0  34943  mblfinlem2  34945  mblfinlem3  34946  ismblfin  34948  itg2addnclem  34958  itg2addnclem2  34959  itg2addnclem3  34960  itg2addnc  34961  ibladdnclem  34963  ftc1cnnclem  34980  ftc1cnnc  34981  ftc1anc  34990  geomcau  35049  prdsbnd  35086  cntotbnd  35089  heiborlem4  35107  rrndstprj2  35124  rrncmslem  35125  rrnequiv  35128  iccbnd  35133  cvlcvr1  36490  cvrat3  36593  dalem25  36849  cdlema1N  36942  dalawlem3  37024  dalawlem4  37025  dalawlem5  37026  dalawlem6  37027  dalawlem7  37028  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  lhp2lt  37152  lhpmcvr  37174  4atexlemcnd  37223  lautj  37244  trlle  37335  trlval3  37338  trlval4  37339  cdleme0moN  37376  cdleme13  37423  cdleme15  37429  cdleme19b  37455  cdleme20e  37464  cdleme20j  37469  cdleme22e  37495  cdleme22eALTN  37496  cdleme26fALTN  37513  cdleme26f  37514  cdleme27N  37520  cdleme41sn3a  37584  cdleme46fsvlpq  37656  cdlemeg46vrg  37678  cdlemg4  37768  cdlemg7N  37777  cdlemg9a  37783  cdlemg11b  37793  cdlemg12a  37794  trljco  37891  tendoidcl  37920  tendococl  37923  tendopltp  37931  tendo0tp  37940  tendoicl  37947  cdlemi2  37970  cdlemk5a  37986  cdlemk5  37987  cdlemk12  38001  cdlemkole  38004  cdlemk14  38005  cdlemk12u  38023  cdlemk37  38065  cdlemk39s-id  38091  cdlemk49  38102  cdlemk39u1  38118  cdlemk39u  38119  dian0  38190  cdlemm10N  38269  cdlemn2  38346  cdlemn10  38357  dihord1  38369  dihord10  38374  dihmeetlem4preN  38457  dihmeetlem18N  38475  dihmeetlem20N  38477  dihjatc  38568  mapdcnvatN  38817  fltltc  39322  lzenom  39416  irrapxlem2  39469  irrapxlem3  39470  irrapxlem5  39472  pellexlem2  39476  pell14qrgt0  39505  pellfundlb  39530  pellfundex  39532  pellfund14  39544  rmspecsqrtnq  39552  jm2.24nn  39605  jm2.17a  39606  jm2.17b  39607  congabseq  39620  acongrep  39626  acongeq  39629  jm2.26lem3  39647  jm2.27a  39651  jm2.27c  39653  hbtlem2  39773  dgraaub  39797  idomodle  39845  relexpxpmin  40111  frege102d  40148  hashnzfzclim  40703  binomcxplemfrat  40732  binomcxplemnotnn0  40737  suprnmpt  41479  mpct  41513  rnmptbddlem  41564  dstregt0  41596  lefldiveq  41608  fzisoeu  41616  upbdrech  41621  ssfiunibd  41625  fzdifsuc2  41626  xadd0ge  41637  supxrgere  41650  supxrge  41655  suplesup  41656  xrlexaddrp  41669  infxrunb2  41685  infleinflem2  41688  reclt0d  41707  infrpgernmpt  41790  ioondisj2  41816  iccshift  41843  iooshift  41847  fmul01  41910  fmul01lt1lem1  41914  fmul01lt1lem2  41915  climrec  41933  climsuse  41938  mullimc  41946  mullimcf  41953  constlimc  41954  idlimc  41956  divcnvg  41957  limcperiod  41958  limcrecl  41959  lptioo2  41961  lptioo1  41962  islpcn  41969  lptre2pt  41970  limcleqr  41974  neglimc  41977  addlimc  41978  0ellimcdiv  41979  limclner  41981  climleltrp  42006  limsuplesup  42029  limsupmnflem  42050  supcnvlimsupmpt  42071  0cnv  42072  xlimconst  42155  xlimliminflimsup  42192  sinaover2ne0  42198  cncfshift  42206  cncfperiod  42211  cncfioobdlem  42228  cncfioobd  42229  fperdvper  42252  dvdivbd  42257  dvbdfbdioolem1  42262  dvbdfbdioolem2  42263  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnmul  42277  dvnprodlem1  42280  itgiccshift  42314  itgperiod  42315  ismbl3  42320  ovolsplit  42322  stoweidlem1  42335  stoweidlem11  42345  stoweidlem13  42347  stoweidlem14  42348  stoweidlem16  42350  stoweidlem21  42355  stoweidlem25  42359  stoweidlem26  42360  stoweidlem36  42370  stoweidlem38  42372  stoweidlem41  42375  stoweidlem42  42376  stoweidlem45  42379  stoweidlem48  42382  stoweidlem52  42386  stoweidlem62  42396  wallispilem3  42401  stirlinglem5  42412  stirlinglem6  42413  stirlinglem7  42414  stirlinglem10  42417  stirlinglem12  42419  stirlinglem15  42422  dirkercncflem1  42437  fourierdlem10  42451  fourierdlem12  42453  fourierdlem15  42456  fourierdlem16  42457  fourierdlem19  42460  fourierdlem20  42461  fourierdlem21  42462  fourierdlem22  42463  fourierdlem24  42465  fourierdlem30  42471  fourierdlem37  42478  fourierdlem39  42480  fourierdlem40  42481  fourierdlem41  42482  fourierdlem42  42483  fourierdlem47  42487  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem52  42492  fourierdlem54  42494  fourierdlem60  42500  fourierdlem61  42501  fourierdlem63  42503  fourierdlem64  42504  fourierdlem68  42508  fourierdlem71  42511  fourierdlem72  42512  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem77  42517  fourierdlem78  42518  fourierdlem79  42519  fourierdlem81  42521  fourierdlem82  42522  fourierdlem83  42523  fourierdlem84  42524  fourierdlem87  42527  fourierdlem92  42532  fourierdlem93  42533  fourierdlem94  42534  fourierdlem101  42541  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  fourierdlem114  42554  sqwvfoura  42562  sqwvfourb  42563  fouriersw  42565  elaa2lem  42567  etransclem23  42591  etransclem28  42596  etransclem32  42600  etransclem35  42603  etransclem48  42616  qndenserrnbllem  42628  rrnprjdstle  42635  ioorrnopnlem  42638  ioorrnopnxrlem  42640  salexct  42666  sge0fsum  42718  sge0supre  42720  sge0rnbnd  42724  sge0lefi  42729  sge0lessmpt  42730  sge0ltfirp  42731  sge0prle  42732  sge0resrnlem  42734  sge0le  42738  sge0split  42740  sge0iunmptlemre  42746  sge0iunmpt  42749  sge0isum  42758  sge0xaddlem1  42764  sge0xaddlem2  42765  sge0xadd  42766  sge0reuz  42778  sge0reuzb  42779  meaunle  42795  meaiunlelem  42799  voliunsge0lem  42803  meaiuninc  42812  meaiininclem  42817  omeunle  42847  omeiunle  42848  omelesplit  42849  omeiunltfirp  42850  carageniuncllem2  42853  caratheodorylem2  42858  caragencmpl  42866  ovnlecvr  42889  ovncvrrp  42895  ovnsubaddlem1  42901  ovnsubadd  42903  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem5  42930  hoidmvle  42931  ovnhoilem1  42932  ovnlecvr2  42941  ovncvr2  42942  hoiqssbllem2  42954  hspmbllem2  42958  hspmbllem3  42959  ovnsplit  42979  ovolval5lem1  42983  vonioolem1  43011  vonioolem2  43012  vonicclem1  43014  vonicclem2  43015  pimconstlt1  43032  smflimlem2  43097  smflimlem4  43099  smfmullem1  43115  smfsuplem1  43134  smflimsuplem4  43146  smflimsuplem5  43147  iccpartltu  43634  iccpartleu  43637  pgrple2abl  44462  difmodm1lt  44631  nnpw2blen  44689  dignn0flhalflem1  44724  2itscp  44817