Theorem eqbrtrd 5092

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 5080	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 256	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  eqbrtrrd  5094  somin2  6029  en1b  8767  en1bOLD  8768  domunsncan  8812  fodomfi  9022  infsupprpr  9193  hartogslem1  9231  wemaplem2  9236  infdifsn  9345  carddomi2  9659  djuinf  9875  carden  10238  alephsuc3  10267  fpwwe2lem5  10322  fpwwe2lem6  10323  inar1  10462  rankcf  10464  lesub3d  11523  lbinfle  11860  supadd  11873  supmul  11877  rpnnen1lem3  12648  divge1  12727  xrmin1  12840  xrmin2  12841  ifle  12860  qbtwnxr  12863  xltnegi  12879  xleadd1a  12916  xlt2add  12923  xlemul1a  12951  xov1plusxeqvd  13159  ubmelm1fzo  13411  flflp1  13455  ceim1l  13495  ceilm1lt  13496  ceille  13498  quoremz  13503  quoremnn0ALT  13505  modlt  13528  modeqmodmin  13589  addmodlteq  13594  seqf1olem1  13690  bernneq  13872  discr  13883  faclbnd2  13933  faclbnd4lem3  13937  hashun2  14026  hashfun  14080  ccatsymb  14215  ccatrn  14222  sqrlem6  14887  sqrlem7  14888  rddif  14980  amgm2  15009  icodiamlt  15075  climconst  15180  rlimconst  15181  serclim0  15214  rlimcn1  15225  mulcn2  15233  reccn2  15234  o1mul  15252  o1rlimmul  15256  iserex  15296  climlec2  15298  iserge0  15300  climcau  15310  caucvgrlem  15312  caucvgr  15315  iseraltlem2  15322  iseraltlem3  15323  iseralt  15324  fsumabs  15441  o1fsum  15453  iserabs  15455  climfsum  15460  isumless  15485  climcndslem2  15490  divrcnv  15492  flo1  15494  supcvg  15496  georeclim  15512  geomulcvg  15516  cvgrat  15523  mertenslem1  15524  prodfclim1  15533  fprodle  15634  efcvgfsum  15723  eftlub  15746  eflegeo  15758  tanhlt1  15797  tanhbnd  15798  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  cos01gt0  15828  ruclem2  15869  ruclem3  15870  ruclem9  15875  ruclem11  15877  ruclem12  15878  bitsfzolem  16069  bitsfzo  16070  bitsinv1lem  16076  sadcaddlem  16092  mulgcd  16184  eucalglt  16218  lcmledvds  16232  lcmfledvds  16265  mulgcddvds  16288  coprmproddvdslem  16295  prmind2  16318  isprm5  16340  divdenle  16381  nonsq  16391  pythagtriplem4  16448  pclem  16467  pcpremul  16472  pczdvds  16492  pcprmpw2  16511  qexpz  16530  prmreclem4  16548  prmreclem5  16549  4sqlem10  16576  ramtub  16641  ramub2  16643  prmodvdslcmf  16676  prmgaplem8  16687  natpropd  17610  catciso  17742  p0le  18062  acsdomd  18190  triv1nsgd  18716  qusgrp  18726  f1otrspeq  18970  pmtrfrn  18981  pmtrfconj  18989  symggen  18993  psgnunilem4  19020  oddvds2  19088  odcau  19124  pgpfi  19125  pgpssslw  19134  sylow3lem4  19150  efgred2  19274  frgp0  19281  odadd2  19365  oddvdssubg  19371  ablfac1c  19589  ablfac1eu  19591  pgpfaclem3  19601  2nsgsimpgd  19620  isabvd  19995  abvsubtri  20010  cyggic  20692  mplsubrg  21121  coe1sfi  21294  mp2pm2mplem5  21867  en2top  22043  1stcrest  22512  2ndcrest  22513  hausmapdom  22559  ufilen  22989  xmetrtri2  23417  prdsxmetlem  23429  bl2in  23461  xblcntrps  23471  xblcntr  23472  ssblps  23483  ssbl  23484  blssps  23485  blss  23486  blcld  23567  methaus  23582  metustexhalf  23618  nmtri2  23689  tngngp3  23726  nrginvrcnlem  23761  nrginvrcn  23762  nmoi  23798  nmo0  23805  nmoid  23812  blcvx  23867  reperflem  23887  reconnlem2  23896  metdcnlem  23905  metdscn  23925  metnrmlem3  23930  mulc1cncf  23974  iccpnfhmeo  24014  cnheiborlem  24023  cnheibor  24024  lebnumii  24035  pcopt  24091  pcopt2  24092  pcoass  24093  nmoleub2lem  24183  nmoleub2lem3  24184  nmoleub2lem2  24185  ipcau2  24303  tcphcphlem1  24304  nglmle  24371  trirn  24469  rrxdstprj1  24478  minveclem3  24498  ivthlem2  24521  ivthlem3  24522  ivth2  24524  ovollb  24548  ovolsslem  24553  ovollb2lem  24557  ovolctb  24559  ovoliunlem1  24571  ovolsca  24584  ovolicc1  24585  ovolicc2lem4  24589  nulmbl  24604  ioombl1lem4  24630  uniioovol  24648  uniioombllem3a  24653  uniioombllem4  24655  opnmbllem  24670  volcn  24675  volivth  24676  i1fadd  24764  i1fmul  24765  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  itg2const2  24811  itg2seq  24812  itg2uba  24813  itg2split  24819  itg2monolem1  24820  itg2monolem3  24822  itg2i1fseq2  24826  itg2addlem  24828  itg2gt0  24830  itg2cnlem1  24831  itg2cnlem2  24832  itgless  24886  ibladdlem  24889  bddmulibl  24908  dveflem  25048  dvferm1lem  25053  dvferm2lem  25055  dvlip  25062  dvlipcn  25063  dvlip2  25064  dvle  25076  dvivthlem1  25077  lhop1lem  25082  dvcvx  25089  dvfsumabs  25092  dvfsumlem2  25096  dvfsumlem4  25098  dvfsumrlim2  25101  dvfsum2  25103  ftc1a  25106  ftc1lem4  25108  ftc1lem5  25109  deg1sub  25178  ply1divex  25206  deg1submon1p  25222  r1pdeglt  25228  dvdsq1p  25230  fta1glem2  25236  fta1g  25237  plyeq0lem  25276  dgrlt  25332  fta1lem  25372  aalioulem2  25398  aalioulem3  25399  aalioulem4  25400  aaliou3lem2  25408  aaliou3lem9  25415  taylply2  25432  ulmbdd  25462  ulmdvlem1  25464  mtest  25468  mtestbdd  25469  radcnvlem1  25477  radcnvle  25484  pserulm  25486  psercn  25490  pserdvlem2  25492  abelthlem2  25496  abelthlem5  25499  abelthlem7  25502  abelthlem8  25503  abelthlem9  25504  reeff1olem  25510  tangtx  25567  tanord  25599  efif1olem4  25606  logrnaddcl  25635  logcj  25666  logimul  25674  logneg2  25675  logdivlti  25680  divlogrlim  25695  logcnlem3  25704  logcnlem4  25705  efopn  25718  logtayllem  25719  logtayl  25720  cxpcn3lem  25805  cxpaddle  25810  abscxpbnd  25811  asinlem3  25926  asinneg  25941  asinsin  25947  atanlogaddlem  25968  atantan  25978  bndatandm  25984  atans2  25986  atantayl  25992  atantayl2  25993  atantayl3  25994  leibpi  25997  birthdaylem3  26008  rlimcnp  26020  efrlim  26024  cxplim  26026  cxp2lim  26031  cxploglim2  26033  divsqrtsumo1  26038  jensenlem2  26042  amgm  26045  logdifbnd  26048  harmonicbnd4  26065  fsumharmonic  26066  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem5  26087  lgambdd  26091  lgamcvg2  26109  ftalem1  26127  ftalem5  26131  basellem1  26135  basellem8  26142  ppip1le  26215  ppiltx  26231  sqff1o  26236  chtublem  26264  chpub  26273  logfaclbnd  26275  logfacrlim  26277  logexprlim  26278  mersenne  26280  bcmono  26330  bcmax  26331  bposlem2  26338  bposlem5  26341  lgslem3  26352  gausslemma2dlem1a  26418  lgsquadlem1  26433  lgsquadlem2  26434  2lgslem1c  26446  2sqblem  26484  chebbnd1  26525  chtppilimlem1  26526  chto1ub  26529  chpchtlim  26532  chpo1ubb  26534  rplogsumlem1  26537  rplogsumlem2  26538  rpvmasumlem  26540  dchrisumlem1  26542  dchrisumlem2  26543  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumlem3  26552  dchrvmasumiflem1  26554  dchrisum0flblem1  26561  dchrisum0fno1  26564  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  rplogsum  26580  mudivsum  26583  mulogsumlem  26584  mulog2sumlem1  26587  mulog2sumlem2  26588  vmalogdivsum2  26591  2vmadivsumlem  26593  selberglem2  26599  selberg2b  26605  logdivbnd  26609  selberg3lem1  26610  selberg3lem2  26611  selberg4lem1  26613  pntrmax  26617  pntrsumo1  26618  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bnd  26637  pntpbnd1a  26638  pntpbnd2  26640  pntibndlem2  26644  pntlemb  26650  pntlemg  26651  pntlemh  26652  pntlemr  26655  pntlemj  26656  pntlemf  26658  pntlemo  26660  pnt  26667  padicabv  26683  ostth2lem2  26687  ostth2lem3  26688  ostth3  26691  colperpexlem3  26997  mideulem2  26999  lnperpex  27068  trgcopy  27069  iscgra1  27075  brbtwn2  27176  colinearalglem4  27180  subupgr  27557  crctcshwlkn0lem1  28076  nvabs  28935  nvge0  28936  smcnlem  28960  nmblolbii  29062  blocnilem  29067  siii  29116  ubthlem2  29134  minvecolem3  29139  htthlem  29180  bcsiALT  29442  bcs3  29446  chscllem4  29903  0cnop  30242  0cnfn  30243  nmbdoplbi  30287  nmcoplbi  30291  nmophmi  30294  nmbdfnlbi  30312  nmcfnlbi  30315  nlelchi  30324  riesz1  30328  cnlnadjlem2  30331  nmopadjlei  30351  nmoptrii  30357  nmopcoi  30358  nmopcoadji  30364  unierri  30367  branmfn  30368  pjs14i  30473  hstle  30493  cdj3lem2b  30700  xlt2addrd  30983  eliccelico  31000  elicoelioo  31001  ltesubnnd  31038  wrdt2ind  31127  archirngz  31345  archiabllem2c  31351  madjusmdetlem2  31680  locfinref  31693  sqsscirc1  31760  tpr2rico  31764  esumcst  31931  esumgect  31958  esum2d  31961  measunl  32084  measiun  32086  omssubaddlem  32166  omssubadd  32167  carsgsigalem  32182  carsgclctunlem2  32186  pmeasmono  32191  eulerpartlemgc  32229  eulerpartlemb  32235  ballotlemsel1i  32379  ballotlemro  32389  sgnsub  32411  signsplypnf  32429  signsply0  32430  signsvtn  32463  signsvfnn  32465  hgt750lemd  32528  logdivsqrle  32530  hashf1dmcdm  32976  erdsze2lem1  33065  sinccvglem  33530  divcnvlin  33604  iprodefisum  33613  faclimlem2  33616  ttrclselem2  33712  nosep1o  33811  nodense  33822  noinfbnd2lem1  33860  noetainflem3  33869  cofcutr  34019  cofcutrtime  34020  fnemeet1  34482  dnibndlem10  34594  dnibndlem11  34595  dnibnd  34598  knoppcnlem4  34603  knoppcnlem6  34605  unblimceq0lem  34613  unbdqndv2lem1  34616  unbdqndv2lem2  34617  knoppndvlem11  34629  knoppndvlem12  34630  knoppndvlem14  34632  knoppndvlem15  34633  knoppndvlem17  34635  knoppndvlem18  34636  knoppndvlem19  34637  knoppndvlem21  34639  ctbssinf  35504  ltflcei  35692  ptrecube  35704  poimirlem16  35720  poimirlem17  35721  poimirlem29  35733  broucube  35738  opnmbllem0  35740  mblfinlem2  35742  mblfinlem3  35743  ismblfin  35745  itg2addnclem  35755  itg2addnclem2  35756  itg2addnclem3  35757  itg2addnc  35758  ibladdnclem  35760  ftc1cnnclem  35775  ftc1cnnc  35776  ftc1anc  35785  geomcau  35844  prdsbnd  35878  cntotbnd  35881  heiborlem4  35899  rrndstprj2  35916  rrncmslem  35917  rrnequiv  35920  iccbnd  35925  cvlcvr1  37280  cvrat3  37383  dalem25  37639  cdlema1N  37732  dalawlem3  37814  dalawlem4  37815  dalawlem5  37816  dalawlem6  37817  dalawlem7  37818  dalawlem9  37820  dalawlem11  37822  dalawlem12  37823  lhp2lt  37942  lhpmcvr  37964  4atexlemcnd  38013  lautj  38034  trlle  38125  trlval3  38128  trlval4  38129  cdleme0moN  38166  cdleme13  38213  cdleme15  38219  cdleme19b  38245  cdleme20e  38254  cdleme20j  38259  cdleme22e  38285  cdleme22eALTN  38286  cdleme26fALTN  38303  cdleme26f  38304  cdleme27N  38310  cdleme41sn3a  38374  cdleme46fsvlpq  38446  cdlemeg46vrg  38468  cdlemg4  38558  cdlemg7N  38567  cdlemg9a  38573  cdlemg11b  38583  cdlemg12a  38584  trljco  38681  tendoidcl  38710  tendococl  38713  tendopltp  38721  tendo0tp  38730  tendoicl  38737  cdlemi2  38760  cdlemk5a  38776  cdlemk5  38777  cdlemk12  38791  cdlemkole  38794  cdlemk14  38795  cdlemk12u  38813  cdlemk37  38855  cdlemk39s-id  38881  cdlemk49  38892  cdlemk39u1  38908  cdlemk39u  38909  dian0  38980  cdlemm10N  39059  cdlemn2  39136  cdlemn10  39147  dihord1  39159  dihord10  39164  dihmeetlem4preN  39247  dihmeetlem18N  39265  dihmeetlem20N  39267  dihjatc  39358  mapdcnvatN  39607  lcmineqlem17  39981  3lexlogpow5ineq2  39991  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  2ap1caineq  40029  sticksstones7  40036  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones12  40042  sticksstones22  40052  metakunt16  40068  metakunt29  40081  fltltc  40414  lzenom  40508  irrapxlem2  40561  irrapxlem3  40562  irrapxlem5  40564  pellexlem2  40568  pell14qrgt0  40597  pellfundlb  40622  pellfundex  40624  pellfund14  40636  rmspecsqrtnq  40644  jm2.24nn  40697  jm2.17a  40698  jm2.17b  40699  congabseq  40712  acongrep  40718  acongeq  40721  jm2.26lem3  40739  jm2.27a  40743  jm2.27c  40745  hbtlem2  40865  dgraaub  40889  idomodle  40937  sqrtcval  41138  relexpxpmin  41214  frege102d  41251  hashnzfzclim  41829  binomcxplemfrat  41858  binomcxplemnotnn0  41863  suprnmpt  42599  mpct  42630  rnmptbddlem  42678  dstregt0  42709  lefldiveq  42721  fzisoeu  42729  upbdrech  42734  ssfiunibd  42738  fzdifsuc2  42739  xadd0ge  42749  supxrgere  42762  supxrge  42767  suplesup  42768  xrlexaddrp  42781  infxrunb2  42797  infleinflem2  42800  reclt0d  42816  infrpgernmpt  42895  ioondisj2  42921  iccshift  42946  iooshift  42950  fmul01  43011  fmul01lt1lem1  43015  fmul01lt1lem2  43016  climrec  43034  climsuse  43039  mullimc  43047  mullimcf  43054  constlimc  43055  idlimc  43057  divcnvg  43058  limcperiod  43059  limcrecl  43060  lptioo2  43062  lptioo1  43063  islpcn  43070  lptre2pt  43071  limcleqr  43075  neglimc  43078  addlimc  43079  0ellimcdiv  43080  limclner  43082  climleltrp  43107  limsuplesup  43130  limsupmnflem  43151  supcnvlimsupmpt  43172  0cnv  43173  xlimconst  43256  xlimliminflimsup  43293  sinaover2ne0  43299  cncfshift  43305  cncfperiod  43310  cncfioobdlem  43327  cncfioobd  43328  fperdvper  43350  dvdivbd  43354  dvbdfbdioolem1  43359  dvbdfbdioolem2  43360  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmul  43374  dvnprodlem1  43377  itgiccshift  43411  itgperiod  43412  ismbl3  43417  ovolsplit  43419  stoweidlem1  43432  stoweidlem11  43442  stoweidlem13  43444  stoweidlem14  43445  stoweidlem16  43447  stoweidlem21  43452  stoweidlem25  43456  stoweidlem26  43457  stoweidlem36  43467  stoweidlem38  43469  stoweidlem41  43472  stoweidlem42  43473  stoweidlem45  43476  stoweidlem48  43479  stoweidlem52  43483  stoweidlem62  43493  wallispilem3  43498  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem10  43514  stirlinglem12  43516  stirlinglem15  43519  dirkercncflem1  43534  fourierdlem10  43548  fourierdlem12  43550  fourierdlem15  43553  fourierdlem16  43554  fourierdlem19  43557  fourierdlem20  43558  fourierdlem21  43559  fourierdlem22  43560  fourierdlem24  43562  fourierdlem30  43568  fourierdlem37  43575  fourierdlem39  43577  fourierdlem40  43578  fourierdlem41  43579  fourierdlem42  43580  fourierdlem47  43584  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem52  43589  fourierdlem54  43591  fourierdlem60  43597  fourierdlem61  43598  fourierdlem63  43600  fourierdlem64  43601  fourierdlem68  43605  fourierdlem71  43608  fourierdlem72  43609  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem77  43614  fourierdlem78  43615  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem83  43620  fourierdlem84  43621  fourierdlem87  43624  fourierdlem92  43629  fourierdlem93  43630  fourierdlem94  43631  fourierdlem101  43638  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  fourierdlem114  43651  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  elaa2lem  43664  etransclem23  43688  etransclem28  43693  etransclem32  43697  etransclem35  43700  etransclem48  43713  qndenserrnbllem  43725  rrnprjdstle  43732  ioorrnopnlem  43735  ioorrnopnxrlem  43737  salexct  43763  sge0fsum  43815  sge0supre  43817  sge0rnbnd  43821  sge0lefi  43826  sge0lessmpt  43827  sge0ltfirp  43828  sge0prle  43829  sge0resrnlem  43831  sge0le  43835  sge0split  43837  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0isum  43855  sge0xaddlem1  43861  sge0xaddlem2  43862  sge0xadd  43863  sge0reuz  43875  sge0reuzb  43876  meaunle  43892  meaiunlelem  43896  voliunsge0lem  43900  meaiuninc  43909  meaiininclem  43914  omeunle  43944  omeiunle  43945  omelesplit  43946  omeiunltfirp  43947  carageniuncllem2  43950  caratheodorylem2  43955  caragencmpl  43963  ovnlecvr  43986  ovncvrrp  43992  ovnsubaddlem1  43998  ovnsubadd  44000  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem5  44027  hoidmvle  44028  ovnhoilem1  44029  ovnlecvr2  44038  ovncvr2  44039  hoiqssbllem2  44051  hspmbllem2  44055  hspmbllem3  44056  ovnsplit  44076  ovolval5lem1  44080  vonioolem1  44108  vonioolem2  44109  vonicclem1  44111  vonicclem2  44112  pimconstlt1  44129  smflimlem2  44194  smflimlem4  44196  smfmullem1  44212  smfsuplem1  44231  smflimsuplem4  44243  smflimsuplem5  44244  iccpartltu  44765  iccpartleu  44768  pgrple2abl  45589  difmodm1lt  45756  nnpw2blen  45814  dignn0flhalflem1  45849  2itscp  46015