Theorem eqbrtrd 5169

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  eqbrtrrd  5171  somin2  6133  en1b  9019  en1bOLD  9020  domunsncan  9068  fodomfi  9321  infsupprpr  9495  hartogslem1  9533  wemaplem2  9538  infdifsn  9648  ttrclselem2  9717  carddomi2  9961  djuinf  10179  carden  10542  alephsuc3  10571  fpwwe2lem5  10626  fpwwe2lem6  10627  inar1  10766  rankcf  10768  lesub3d  11828  lbinfle  12165  supadd  12178  supmul  12182  rpnnen1lem3  12959  divge1  13038  xrmin1  13152  xrmin2  13153  ifle  13172  qbtwnxr  13175  xltnegi  13191  xleadd1a  13228  xlt2add  13235  xlemul1a  13263  xov1plusxeqvd  13471  ubmelm1fzo  13724  flflp1  13768  ceim1l  13808  ceilm1lt  13809  ceille  13811  quoremz  13816  quoremnn0ALT  13818  modlt  13841  modeqmodmin  13902  addmodlteq  13907  seqf1olem1  14003  bernneq  14188  discr  14199  faclbnd2  14247  faclbnd4lem3  14251  hashun2  14339  hashfun  14393  ccatsymb  14528  ccatrn  14535  01sqrexlem6  15190  01sqrexlem7  15191  rddif  15283  amgm2  15312  icodiamlt  15378  climconst  15483  rlimconst  15484  serclim0  15517  rlimcn1  15528  mulcn2  15536  reccn2  15537  o1mul  15555  o1rlimmul  15559  iserex  15599  climlec2  15601  iserge0  15603  climcau  15613  caucvgrlem  15615  caucvgr  15618  iseraltlem2  15625  iseraltlem3  15626  iseralt  15627  fsumabs  15743  o1fsum  15755  iserabs  15757  climfsum  15762  isumless  15787  climcndslem2  15792  divrcnv  15794  flo1  15796  supcvg  15798  georeclim  15814  geomulcvg  15818  cvgrat  15825  mertenslem1  15826  prodfclim1  15835  fprodle  15936  efcvgfsum  16025  eftlub  16048  eflegeo  16060  tanhlt1  16099  tanhbnd  16100  ef01bndlem  16123  sin01bnd  16124  cos01bnd  16125  cos01gt0  16130  ruclem2  16171  ruclem3  16172  ruclem9  16177  ruclem11  16179  ruclem12  16180  bitsfzolem  16371  bitsfzo  16372  bitsinv1lem  16378  sadcaddlem  16394  mulgcd  16486  eucalglt  16518  lcmledvds  16532  lcmfledvds  16565  mulgcddvds  16588  coprmproddvdslem  16595  prmind2  16618  isprm5  16640  divdenle  16681  nonsq  16691  pythagtriplem4  16748  pclem  16767  pcpremul  16772  pczdvds  16792  pcprmpw2  16811  qexpz  16830  prmreclem4  16848  prmreclem5  16849  4sqlem10  16876  ramtub  16941  ramub2  16943  prmodvdslcmf  16976  prmgaplem8  16987  natpropd  17925  catciso  18057  p0le  18378  acsdomd  18506  triv1nsgd  19047  qusgrp  19059  f1otrspeq  19308  pmtrfrn  19319  pmtrfconj  19327  symggen  19331  psgnunilem4  19358  oddvds2  19427  odcau  19465  pgpfi  19466  pgpssslw  19475  sylow3lem4  19491  efgred2  19614  frgp0  19621  odadd2  19709  oddvdssubg  19715  ablfac1c  19933  ablfac1eu  19935  pgpfaclem3  19945  2nsgsimpgd  19964  isabvd  20416  abvsubtri  20431  cyggic  21112  mplsubrg  21546  coe1sfi  21719  mp2pm2mplem5  22294  en2top  22470  1stcrest  22939  2ndcrest  22940  hausmapdom  22986  ufilen  23416  xmetrtri2  23844  prdsxmetlem  23856  bl2in  23888  xblcntrps  23898  xblcntr  23899  ssblps  23910  ssbl  23911  blssps  23912  blss  23913  blcld  23996  methaus  24011  metustexhalf  24047  nmtri2  24118  tngngp3  24155  nrginvrcnlem  24190  nrginvrcn  24191  nmoi  24227  nmo0  24234  nmoid  24241  blcvx  24296  reperflem  24316  reconnlem2  24325  metdcnlem  24334  metdscn  24354  metnrmlem3  24359  mulc1cncf  24403  iccpnfhmeo  24443  cnheiborlem  24452  cnheibor  24453  lebnumii  24464  pcopt  24520  pcopt2  24521  pcoass  24522  nmoleub2lem  24612  nmoleub2lem3  24613  nmoleub2lem2  24614  ipcau2  24733  tcphcphlem1  24734  nglmle  24801  trirn  24899  rrxdstprj1  24908  minveclem3  24928  ivthlem2  24951  ivthlem3  24952  ivth2  24954  ovollb  24978  ovolsslem  24983  ovollb2lem  24987  ovolctb  24989  ovoliunlem1  25001  ovolsca  25014  ovolicc1  25015  ovolicc2lem4  25019  nulmbl  25034  ioombl1lem4  25060  uniioovol  25078  uniioombllem3a  25083  uniioombllem4  25085  opnmbllem  25100  volcn  25105  volivth  25106  i1fadd  25194  i1fmul  25195  mbfi1fseqlem4  25218  mbfi1fseqlem5  25219  mbfi1fseqlem6  25220  itg2const2  25241  itg2seq  25242  itg2uba  25243  itg2split  25249  itg2monolem1  25250  itg2monolem3  25252  itg2i1fseq2  25256  itg2addlem  25258  itg2gt0  25260  itg2cnlem1  25261  itg2cnlem2  25262  itgless  25316  ibladdlem  25319  bddmulibl  25338  dveflem  25478  dvferm1lem  25483  dvferm2lem  25485  dvlip  25492  dvlipcn  25493  dvlip2  25494  dvle  25506  dvivthlem1  25507  lhop1lem  25512  dvcvx  25519  dvfsumabs  25522  dvfsumlem2  25526  dvfsumlem4  25528  dvfsumrlim2  25531  dvfsum2  25533  ftc1a  25536  ftc1lem4  25538  ftc1lem5  25539  deg1sub  25608  ply1divex  25636  deg1submon1p  25652  r1pdeglt  25658  dvdsq1p  25660  fta1glem2  25666  fta1g  25667  plyeq0lem  25706  dgrlt  25762  fta1lem  25802  aalioulem2  25828  aalioulem3  25829  aalioulem4  25830  aaliou3lem2  25838  aaliou3lem9  25845  taylply2  25862  ulmbdd  25892  ulmdvlem1  25894  mtest  25898  mtestbdd  25899  radcnvlem1  25907  radcnvle  25914  pserulm  25916  psercn  25920  pserdvlem2  25922  abelthlem2  25926  abelthlem5  25929  abelthlem7  25932  abelthlem8  25933  abelthlem9  25934  reeff1olem  25940  tangtx  25997  tanord  26029  efif1olem4  26036  logrnaddcl  26065  logcj  26096  logimul  26104  logneg2  26105  logdivlti  26110  divlogrlim  26125  logcnlem3  26134  logcnlem4  26135  efopn  26148  logtayllem  26149  logtayl  26150  cxpcn3lem  26235  cxpaddle  26240  abscxpbnd  26241  asinlem3  26356  asinneg  26371  asinsin  26377  atanlogaddlem  26398  atantan  26408  bndatandm  26414  atans2  26416  atantayl  26422  atantayl2  26423  atantayl3  26424  leibpi  26427  birthdaylem3  26438  rlimcnp  26450  efrlim  26454  cxplim  26456  cxp2lim  26461  cxploglim2  26463  divsqrtsumo1  26468  jensenlem2  26472  amgm  26475  logdifbnd  26478  harmonicbnd4  26495  fsumharmonic  26496  lgamgulmlem2  26514  lgamgulmlem3  26515  lgamgulmlem5  26517  lgambdd  26521  lgamcvg2  26539  ftalem1  26557  ftalem5  26561  basellem1  26565  basellem8  26572  ppip1le  26645  ppiltx  26661  sqff1o  26666  chtublem  26694  chpub  26703  logfaclbnd  26705  logfacrlim  26707  logexprlim  26708  mersenne  26710  bcmono  26760  bcmax  26761  bposlem2  26768  bposlem5  26771  lgslem3  26782  gausslemma2dlem1a  26848  lgsquadlem1  26863  lgsquadlem2  26864  2lgslem1c  26876  2sqblem  26914  chebbnd1  26955  chtppilimlem1  26956  chto1ub  26959  chpchtlim  26962  chpo1ubb  26964  rplogsumlem1  26967  rplogsumlem2  26968  rpvmasumlem  26970  dchrisumlem1  26972  dchrisumlem2  26973  dchrmusum2  26977  dchrvmasumlem2  26981  dchrvmasumlem3  26982  dchrvmasumiflem1  26984  dchrisum0flblem1  26991  dchrisum0fno1  26994  dchrisum0lem1b  26998  dchrisum0lem1  26999  dchrisum0lem2a  27000  dchrisum0lem2  27001  rplogsum  27010  mudivsum  27013  mulogsumlem  27014  mulog2sumlem1  27017  mulog2sumlem2  27018  vmalogdivsum2  27021  2vmadivsumlem  27023  selberglem2  27029  selberg2b  27035  logdivbnd  27039  selberg3lem1  27040  selberg3lem2  27041  selberg4lem1  27043  pntrmax  27047  pntrsumo1  27048  pntrlog2bndlem1  27060  pntrlog2bndlem2  27061  pntrlog2bndlem3  27062  pntrlog2bndlem4  27063  pntrlog2bndlem5  27064  pntrlog2bnd  27067  pntpbnd1a  27068  pntpbnd2  27070  pntibndlem2  27074  pntlemb  27080  pntlemg  27081  pntlemh  27082  pntlemr  27085  pntlemj  27086  pntlemf  27088  pntlemo  27090  pnt  27097  padicabv  27113  ostth2lem2  27117  ostth2lem3  27118  ostth3  27121  nosep1o  27164  nodense  27175  noinfbnd2lem1  27213  noetainflem3  27222  mins1  27250  mins2  27251  cofcutr  27391  cofcutrtime  27394  addsuniflem  27464  negsunif  27509  ssltmul1  27582  mulsuniflem  27584  precsexlem11  27643  colperpexlem3  27963  mideulem2  27965  lnperpex  28034  trgcopy  28035  iscgra1  28041  brbtwn2  28143  colinearalglem4  28147  subupgr  28524  crctcshwlkn0lem1  29044  nvabs  29903  nvge0  29904  smcnlem  29928  nmblolbii  30030  blocnilem  30035  siii  30084  ubthlem2  30102  minvecolem3  30107  htthlem  30148  bcsiALT  30410  bcs3  30414  chscllem4  30871  0cnop  31210  0cnfn  31211  nmbdoplbi  31255  nmcoplbi  31259  nmophmi  31262  nmbdfnlbi  31280  nmcfnlbi  31283  nlelchi  31292  riesz1  31296  cnlnadjlem2  31299  nmopadjlei  31319  nmoptrii  31325  nmopcoi  31326  nmopcoadji  31332  unierri  31335  branmfn  31336  pjs14i  31441  hstle  31461  cdj3lem2b  31668  xlt2addrd  31949  eliccelico  31966  elicoelioo  31967  ltesubnnd  32006  wrdt2ind  32095  archirngz  32313  archiabllem2c  32319  ply1degltel  32613  ply1degltdimlem  32652  madjusmdetlem2  32746  locfinref  32759  sqsscirc1  32826  tpr2rico  32830  esumcst  32999  esumgect  33026  esum2d  33029  measunl  33152  measiun  33154  omssubaddlem  33236  omssubadd  33237  carsgsigalem  33252  carsgclctunlem2  33256  pmeasmono  33261  eulerpartlemgc  33299  eulerpartlemb  33305  ballotlemsel1i  33449  ballotlemro  33459  sgnsub  33481  signsplypnf  33499  signsply0  33500  signsvtn  33533  signsvfnn  33535  hgt750lemd  33598  logdivsqrle  33600  hashf1dmcdm  34043  erdsze2lem1  34132  sinccvglem  34595  divcnvlin  34640  iprodefisum  34649  faclimlem2  34652  gg-dvfsumlem2  35121  fnemeet1  35189  dnibndlem10  35301  dnibndlem11  35302  dnibnd  35305  knoppcnlem4  35310  knoppcnlem6  35312  unblimceq0lem  35320  unbdqndv2lem1  35323  unbdqndv2lem2  35324  knoppndvlem11  35336  knoppndvlem12  35337  knoppndvlem14  35339  knoppndvlem15  35340  knoppndvlem17  35342  knoppndvlem18  35343  knoppndvlem19  35344  knoppndvlem21  35346  ctbssinf  36225  ltflcei  36414  ptrecube  36426  poimirlem16  36442  poimirlem17  36443  poimirlem29  36455  broucube  36460  opnmbllem0  36462  mblfinlem2  36464  mblfinlem3  36465  ismblfin  36467  itg2addnclem  36477  itg2addnclem2  36478  itg2addnclem3  36479  itg2addnc  36480  ibladdnclem  36482  ftc1cnnclem  36497  ftc1cnnc  36498  ftc1anc  36507  geomcau  36565  prdsbnd  36599  cntotbnd  36602  heiborlem4  36620  rrndstprj2  36637  rrncmslem  36638  rrnequiv  36641  iccbnd  36646  cvlcvr1  38147  cvrat3  38251  dalem25  38507  cdlema1N  38600  dalawlem3  38682  dalawlem4  38683  dalawlem5  38684  dalawlem6  38685  dalawlem7  38686  dalawlem9  38688  dalawlem11  38690  dalawlem12  38691  lhp2lt  38810  lhpmcvr  38832  4atexlemcnd  38881  lautj  38902  trlle  38993  trlval3  38996  trlval4  38997  cdleme0moN  39034  cdleme13  39081  cdleme15  39087  cdleme19b  39113  cdleme20e  39122  cdleme20j  39127  cdleme22e  39153  cdleme22eALTN  39154  cdleme26fALTN  39171  cdleme26f  39172  cdleme27N  39178  cdleme41sn3a  39242  cdleme46fsvlpq  39314  cdlemeg46vrg  39336  cdlemg4  39426  cdlemg7N  39435  cdlemg9a  39441  cdlemg11b  39451  cdlemg12a  39452  trljco  39549  tendoidcl  39578  tendococl  39581  tendopltp  39589  tendo0tp  39598  tendoicl  39605  cdlemi2  39628  cdlemk5a  39644  cdlemk5  39645  cdlemk12  39659  cdlemkole  39662  cdlemk14  39663  cdlemk12u  39681  cdlemk37  39723  cdlemk39s-id  39749  cdlemk49  39760  cdlemk39u1  39776  cdlemk39u  39777  dian0  39848  cdlemm10N  39927  cdlemn2  40004  cdlemn10  40015  dihord1  40027  dihord10  40032  dihmeetlem4preN  40115  dihmeetlem18N  40133  dihmeetlem20N  40135  dihjatc  40226  mapdcnvatN  40475  lcmineqlem17  40848  3lexlogpow5ineq2  40858  3lexlogpow2ineq2  40862  3lexlogpow5ineq5  40863  aks4d1p1p3  40872  aks4d1p1p2  40873  aks4d1p1p4  40874  aks4d1p1p7  40877  aks4d1p1p5  40878  aks4d1p1  40879  aks4d1p3  40881  aks4d1p5  40883  aks4d1p6  40884  aks4d1p7d1  40885  aks4d1p7  40886  aks4d1p8  40890  2ap1caineq  40899  sticksstones7  40906  sticksstones10  40909  sticksstones11  40910  sticksstones12a  40911  sticksstones12  40912  sticksstones22  40922  metakunt16  40938  metakunt29  40951  evlselv  41109  fltltc  41347  lzenom  41441  irrapxlem2  41494  irrapxlem3  41495  irrapxlem5  41497  pellexlem2  41501  pell14qrgt0  41530  pellfundlb  41555  pellfundex  41557  pellfund14  41569  rmspecsqrtnq  41577  jm2.24nn  41631  jm2.17a  41632  jm2.17b  41633  congabseq  41646  acongrep  41652  acongeq  41655  jm2.26lem3  41673  jm2.27a  41677  jm2.27c  41679  hbtlem2  41799  dgraaub  41823  idomodle  41871  safesnsupfidom1o  42101  sqrtcval  42325  relexpxpmin  42401  frege102d  42438  hashnzfzclim  43014  binomcxplemfrat  43043  binomcxplemnotnn0  43048  suprnmpt  43803  mpct  43833  rnmptbddlem  43882  dstregt0  43926  lefldiveq  43937  fzisoeu  43945  upbdrech  43950  ssfiunibd  43954  fzdifsuc2  43955  xadd0ge  43965  supxrgere  43978  supxrge  43983  suplesup  43984  xrlexaddrp  43997  infxrunb2  44013  infleinflem2  44016  reclt0d  44032  infrpgernmpt  44110  rexanuz2nf  44138  ioondisj2  44141  iccshift  44166  iooshift  44170  fmul01  44231  fmul01lt1lem1  44235  fmul01lt1lem2  44236  climrec  44254  climsuse  44259  mullimc  44267  mullimcf  44274  constlimc  44275  idlimc  44277  divcnvg  44278  limcperiod  44279  limcrecl  44280  lptioo2  44282  lptioo1  44283  islpcn  44290  lptre2pt  44291  limcleqr  44295  neglimc  44298  addlimc  44299  0ellimcdiv  44300  limclner  44302  climleltrp  44327  limsuplesup  44350  limsupmnflem  44371  supcnvlimsupmpt  44392  0cnv  44393  xlimconst  44476  xlimliminflimsup  44513  sinaover2ne0  44519  cncfshift  44525  cncfperiod  44530  cncfioobdlem  44547  cncfioobd  44548  fperdvper  44570  dvdivbd  44574  dvbdfbdioolem1  44579  dvbdfbdioolem2  44580  ioodvbdlimc1lem1  44582  ioodvbdlimc1lem2  44583  ioodvbdlimc2lem  44585  dvnmul  44594  dvnprodlem1  44597  itgiccshift  44631  itgperiod  44632  ismbl3  44637  ovolsplit  44639  stoweidlem1  44652  stoweidlem11  44662  stoweidlem13  44664  stoweidlem14  44665  stoweidlem16  44667  stoweidlem21  44672  stoweidlem25  44676  stoweidlem26  44677  stoweidlem36  44687  stoweidlem38  44689  stoweidlem41  44692  stoweidlem42  44693  stoweidlem45  44696  stoweidlem48  44699  stoweidlem52  44703  stoweidlem62  44713  wallispilem3  44718  stirlinglem5  44729  stirlinglem6  44730  stirlinglem7  44731  stirlinglem10  44734  stirlinglem12  44736  stirlinglem15  44739  dirkercncflem1  44754  fourierdlem10  44768  fourierdlem12  44770  fourierdlem15  44773  fourierdlem16  44774  fourierdlem19  44777  fourierdlem20  44778  fourierdlem21  44779  fourierdlem22  44780  fourierdlem24  44782  fourierdlem30  44788  fourierdlem37  44795  fourierdlem39  44797  fourierdlem40  44798  fourierdlem41  44799  fourierdlem42  44800  fourierdlem47  44804  fourierdlem48  44805  fourierdlem49  44806  fourierdlem50  44807  fourierdlem52  44809  fourierdlem54  44811  fourierdlem60  44817  fourierdlem61  44818  fourierdlem63  44820  fourierdlem64  44821  fourierdlem68  44825  fourierdlem71  44828  fourierdlem72  44829  fourierdlem73  44830  fourierdlem74  44831  fourierdlem75  44832  fourierdlem76  44833  fourierdlem77  44834  fourierdlem78  44835  fourierdlem79  44836  fourierdlem81  44838  fourierdlem82  44839  fourierdlem83  44840  fourierdlem84  44841  fourierdlem87  44844  fourierdlem92  44849  fourierdlem93  44850  fourierdlem94  44851  fourierdlem101  44858  fourierdlem102  44859  fourierdlem103  44860  fourierdlem104  44861  fourierdlem111  44868  fourierdlem112  44869  fourierdlem113  44870  fourierdlem114  44871  sqwvfoura  44879  sqwvfourb  44880  fouriersw  44882  elaa2lem  44884  etransclem23  44908  etransclem28  44913  etransclem32  44917  etransclem35  44920  etransclem48  44933  qndenserrnbllem  44945  rrnprjdstle  44952  ioorrnopnlem  44955  ioorrnopnxrlem  44957  salexct  44985  sge0fsum  45038  sge0supre  45040  sge0rnbnd  45044  sge0lefi  45049  sge0lessmpt  45050  sge0ltfirp  45051  sge0prle  45052  sge0resrnlem  45054  sge0le  45058  sge0split  45060  sge0iunmptlemre  45066  sge0iunmpt  45069  sge0isum  45078  sge0xaddlem1  45084  sge0xaddlem2  45085  sge0xadd  45086  sge0reuz  45098  sge0reuzb  45099  meaunle  45115  meaiunlelem  45119  voliunsge0lem  45123  meaiuninc  45132  meaiininclem  45137  omeunle  45167  omeiunle  45168  omelesplit  45169  omeiunltfirp  45170  carageniuncllem2  45173  caratheodorylem2  45178  caragencmpl  45186  ovnlecvr  45209  ovncvrrp  45215  ovnsubaddlem1  45221  ovnsubadd  45223  hoidmv1lelem1  45242  hoidmv1lelem2  45243  hoidmv1le  45245  hoidmvlelem1  45246  hoidmvlelem2  45247  hoidmvlelem5  45250  hoidmvle  45251  ovnhoilem1  45252  ovnlecvr2  45261  ovncvr2  45262  hoiqssbllem2  45274  hspmbllem2  45278  hspmbllem3  45279  ovnsplit  45299  ovolval5lem1  45303  vonioolem1  45331  vonioolem2  45332  vonicclem1  45334  vonicclem2  45335  pimconstlt1  45353  smflimlem2  45423  smflimlem4  45425  smfmullem1  45442  smfsuplem1  45462  smflimsuplem4  45474  smflimsuplem5  45475  upwordnul  45529  iccpartltu  46028  iccpartleu  46031  pgrple2abl  46943  difmodm1lt  47110  nnpw2blen  47168  dignn0flhalflem1  47203  2itscp  47369