Theorem eqbrtrd 5170

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5148

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  eqbrtrrd  5172  somin2  6136  en1b  9029  en1bOLD  9030  domunsncan  9078  fodomfi  9331  infsupprpr  9505  hartogslem1  9543  wemaplem2  9548  infdifsn  9658  ttrclselem2  9727  carddomi2  9971  djuinf  10189  carden  10552  alephsuc3  10581  fpwwe2lem5  10636  fpwwe2lem6  10637  inar1  10776  rankcf  10778  lesub3d  11839  lbinfle  12176  supadd  12189  supmul  12193  rpnnen1lem3  12970  divge1  13049  xrmin1  13163  xrmin2  13164  ifle  13183  qbtwnxr  13186  xltnegi  13202  xleadd1a  13239  xlt2add  13246  xlemul1a  13274  xov1plusxeqvd  13482  ubmelm1fzo  13735  flflp1  13779  ceim1l  13819  ceilm1lt  13820  ceille  13822  quoremz  13827  quoremnn0ALT  13829  modlt  13852  modeqmodmin  13913  addmodlteq  13918  seqf1olem1  14014  bernneq  14199  discr  14210  faclbnd2  14258  faclbnd4lem3  14262  hashun2  14350  hashfun  14404  ccatsymb  14539  ccatrn  14546  01sqrexlem6  15201  01sqrexlem7  15202  rddif  15294  amgm2  15323  icodiamlt  15389  climconst  15494  rlimconst  15495  serclim0  15528  rlimcn1  15539  mulcn2  15547  reccn2  15548  o1mul  15566  o1rlimmul  15570  iserex  15610  climlec2  15612  iserge0  15614  climcau  15624  caucvgrlem  15626  caucvgr  15629  iseraltlem2  15636  iseraltlem3  15637  iseralt  15638  fsumabs  15754  o1fsum  15766  iserabs  15768  climfsum  15773  isumless  15798  climcndslem2  15803  divrcnv  15805  flo1  15807  supcvg  15809  georeclim  15825  geomulcvg  15829  cvgrat  15836  mertenslem1  15837  prodfclim1  15846  fprodle  15947  efcvgfsum  16036  eftlub  16059  eflegeo  16071  tanhlt1  16110  tanhbnd  16111  ef01bndlem  16134  sin01bnd  16135  cos01bnd  16136  cos01gt0  16141  ruclem2  16182  ruclem3  16183  ruclem9  16188  ruclem11  16190  ruclem12  16191  bitsfzolem  16382  bitsfzo  16383  bitsinv1lem  16389  sadcaddlem  16405  mulgcd  16497  eucalglt  16529  lcmledvds  16543  lcmfledvds  16576  mulgcddvds  16599  coprmproddvdslem  16606  prmind2  16629  isprm5  16651  divdenle  16692  nonsq  16702  pythagtriplem4  16759  pclem  16778  pcpremul  16783  pczdvds  16803  pcprmpw2  16822  qexpz  16841  prmreclem4  16859  prmreclem5  16860  4sqlem10  16887  ramtub  16952  ramub2  16954  prmodvdslcmf  16987  prmgaplem8  16998  natpropd  17939  catciso  18071  p0le  18392  acsdomd  18520  triv1nsgd  19096  qusgrp  19108  f1otrspeq  19363  pmtrfrn  19374  pmtrfconj  19382  symggen  19386  psgnunilem4  19413  oddvds2  19482  odcau  19520  pgpfi  19521  pgpssslw  19530  sylow3lem4  19546  efgred2  19669  frgp0  19676  odadd2  19765  oddvdssubg  19771  ablfac1c  19989  ablfac1eu  19991  pgpfaclem3  20001  2nsgsimpgd  20020  isabvd  20659  abvsubtri  20674  cyggic  21439  mplsubrg  21876  psdmplcl  22015  coe1sfi  22057  mp2pm2mplem5  22633  en2top  22809  1stcrest  23278  2ndcrest  23279  hausmapdom  23325  ufilen  23755  xmetrtri2  24183  prdsxmetlem  24195  bl2in  24227  xblcntrps  24237  xblcntr  24238  ssblps  24249  ssbl  24250  blssps  24251  blss  24252  blcld  24335  methaus  24350  metustexhalf  24386  nmtri2  24457  tngngp3  24494  nrginvrcnlem  24529  nrginvrcn  24530  nmoi  24566  nmo0  24573  nmoid  24580  blcvx  24635  reperflem  24655  reconnlem2  24664  metdcnlem  24673  metdscn  24693  metnrmlem3  24698  mulc1cncf  24746  iccpnfhmeo  24791  cnheiborlem  24801  cnheibor  24802  lebnumii  24813  pcopt  24870  pcopt2  24871  pcoass  24872  nmoleub2lem  24962  nmoleub2lem3  24963  nmoleub2lem2  24964  ipcau2  25083  tcphcphlem1  25084  nglmle  25151  trirn  25249  rrxdstprj1  25258  minveclem3  25278  ivthlem2  25302  ivthlem3  25303  ivth2  25305  ovollb  25329  ovolsslem  25334  ovollb2lem  25338  ovolctb  25340  ovoliunlem1  25352  ovolsca  25365  ovolicc1  25366  ovolicc2lem4  25370  nulmbl  25385  ioombl1lem4  25411  uniioovol  25429  uniioombllem3a  25434  uniioombllem4  25436  opnmbllem  25451  volcn  25456  volivth  25457  i1fadd  25545  i1fmul  25546  mbfi1fseqlem4  25569  mbfi1fseqlem5  25570  mbfi1fseqlem6  25571  itg2const2  25592  itg2seq  25593  itg2uba  25594  itg2split  25600  itg2monolem1  25601  itg2monolem3  25603  itg2i1fseq2  25607  itg2addlem  25609  itg2gt0  25611  itg2cnlem1  25612  itg2cnlem2  25613  itgless  25667  ibladdlem  25670  bddmulibl  25689  dveflem  25832  dvferm1lem  25837  dvferm2lem  25839  dvlip  25847  dvlipcn  25848  dvlip2  25849  dvle  25861  dvivthlem1  25862  lhop1lem  25867  dvcvx  25874  dvfsumabs  25878  dvfsumlem2  25882  dvfsumlem2OLD  25883  dvfsumlem4  25885  dvfsumrlim2  25888  dvfsum2  25890  ftc1a  25893  ftc1lem4  25895  ftc1lem5  25896  deg1sub  25965  ply1divex  25993  deg1submon1p  26009  r1pdeglt  26015  dvdsq1p  26017  fta1glem2  26023  fta1g  26024  plyeq0lem  26063  dgrlt  26120  fta1lem  26160  aalioulem2  26186  aalioulem3  26187  aalioulem4  26188  aaliou3lem2  26196  aaliou3lem9  26203  taylply2  26220  ulmbdd  26250  ulmdvlem1  26252  mtest  26256  mtestbdd  26257  radcnvlem1  26265  radcnvle  26272  pserulm  26274  psercn  26279  pserdvlem2  26281  abelthlem2  26285  abelthlem5  26288  abelthlem7  26291  abelthlem8  26292  abelthlem9  26293  reeff1olem  26299  tangtx  26356  tanord  26388  efif1olem4  26395  logrnaddcl  26424  logcj  26455  logimul  26463  logneg2  26464  logdivlti  26469  divlogrlim  26484  logcnlem3  26493  logcnlem4  26494  efopn  26507  logtayllem  26508  logtayl  26509  cxpcn3lem  26597  cxpaddle  26602  abscxpbnd  26603  asinlem3  26718  asinneg  26733  asinsin  26739  atanlogaddlem  26760  atantan  26770  bndatandm  26776  atans2  26778  atantayl  26784  atantayl2  26785  atantayl3  26786  leibpi  26789  birthdaylem3  26800  rlimcnp  26812  efrlim  26816  efrlimOLD  26817  cxplim  26819  cxp2lim  26824  cxploglim2  26826  divsqrtsumo1  26831  jensenlem2  26835  amgm  26838  logdifbnd  26841  harmonicbnd4  26858  fsumharmonic  26859  lgamgulmlem2  26877  lgamgulmlem3  26878  lgamgulmlem5  26880  lgambdd  26884  lgamcvg2  26902  ftalem1  26920  ftalem5  26924  basellem1  26928  basellem8  26935  ppip1le  27008  ppiltx  27024  sqff1o  27029  chtublem  27059  chpub  27068  logfaclbnd  27070  logfacrlim  27072  logexprlim  27073  mersenne  27075  bcmono  27125  bcmax  27126  bposlem2  27133  bposlem5  27136  lgslem3  27147  gausslemma2dlem1a  27213  lgsquadlem1  27228  lgsquadlem2  27229  2lgslem1c  27241  2sqblem  27279  chebbnd1  27320  chtppilimlem1  27321  chto1ub  27324  chpchtlim  27327  chpo1ubb  27329  rplogsumlem1  27332  rplogsumlem2  27333  rpvmasumlem  27335  dchrisumlem1  27337  dchrisumlem2  27338  dchrmusum2  27342  dchrvmasumlem2  27346  dchrvmasumlem3  27347  dchrvmasumiflem1  27349  dchrisum0flblem1  27356  dchrisum0fno1  27359  dchrisum0lem1b  27363  dchrisum0lem1  27364  dchrisum0lem2a  27365  dchrisum0lem2  27366  rplogsum  27375  mudivsum  27378  mulogsumlem  27379  mulog2sumlem1  27382  mulog2sumlem2  27383  vmalogdivsum2  27386  2vmadivsumlem  27388  selberglem2  27394  selberg2b  27400  logdivbnd  27404  selberg3lem1  27405  selberg3lem2  27406  selberg4lem1  27408  pntrmax  27412  pntrsumo1  27413  pntrlog2bndlem1  27425  pntrlog2bndlem2  27426  pntrlog2bndlem3  27427  pntrlog2bndlem4  27428  pntrlog2bndlem5  27429  pntrlog2bnd  27432  pntpbnd1a  27433  pntpbnd2  27435  pntibndlem2  27439  pntlemb  27445  pntlemg  27446  pntlemh  27447  pntlemr  27450  pntlemj  27451  pntlemf  27453  pntlemo  27455  pnt  27462  padicabv  27478  ostth2lem2  27482  ostth2lem3  27483  ostth3  27486  nosep1o  27529  nodense  27540  noinfbnd2lem1  27578  noetainflem3  27587  mins1  27615  mins2  27616  cofcutr  27759  cofcutrtime  27762  addsuniflem  27833  negsunif  27882  ssltmul1  27962  mulsuniflem  27964  precsexlem11  28030  readdscl  28109  remulscllem2  28111  colperpexlem3  28418  mideulem2  28420  lnperpex  28489  trgcopy  28490  iscgra1  28496  brbtwn2  28598  colinearalglem4  28602  subupgr  28979  crctcshwlkn0lem1  29499  nvabs  30360  nvge0  30361  smcnlem  30385  nmblolbii  30487  blocnilem  30492  siii  30541  ubthlem2  30559  minvecolem3  30564  htthlem  30605  bcsiALT  30867  bcs3  30871  chscllem4  31328  0cnop  31667  0cnfn  31668  nmbdoplbi  31712  nmcoplbi  31716  nmophmi  31719  nmbdfnlbi  31737  nmcfnlbi  31740  nlelchi  31749  riesz1  31753  cnlnadjlem2  31756  nmopadjlei  31776  nmoptrii  31782  nmopcoi  31783  nmopcoadji  31789  unierri  31792  branmfn  31793  pjs14i  31898  hstle  31918  cdj3lem2b  32125  xlt2addrd  32406  eliccelico  32423  elicoelioo  32424  ltesubnnd  32463  wrdt2ind  32552  archirngz  32773  archiabllem2c  32779  ply1degltel  33108  ply1degleel  33109  ig1pmindeg  33115  q1pdir  33116  ply1degltdimlem  33163  minplyirredlem  33226  algextdeglem6  33235  madjusmdetlem2  33274  locfinref  33287  sqsscirc1  33354  tpr2rico  33358  esumcst  33527  esumgect  33554  esum2d  33557  measunl  33680  measiun  33682  omssubaddlem  33764  omssubadd  33765  carsgsigalem  33780  carsgclctunlem2  33784  pmeasmono  33789  eulerpartlemgc  33827  eulerpartlemb  33833  ballotlemsel1i  33977  ballotlemro  33987  sgnsub  34009  signsplypnf  34027  signsply0  34028  signsvtn  34061  signsvfnn  34063  hgt750lemd  34126  logdivsqrle  34128  hashf1dmcdm  34571  erdsze2lem1  34660  sinccvglem  35123  divcnvlin  35174  iprodefisum  35183  faclimlem2  35186  fnemeet1  35718  dnibndlem10  35830  dnibndlem11  35831  dnibnd  35834  knoppcnlem4  35839  knoppcnlem6  35841  unblimceq0lem  35849  unbdqndv2lem1  35852  unbdqndv2lem2  35853  knoppndvlem11  35865  knoppndvlem12  35866  knoppndvlem14  35868  knoppndvlem15  35869  knoppndvlem17  35871  knoppndvlem18  35872  knoppndvlem19  35873  knoppndvlem21  35875  ctbssinf  36754  ltflcei  36943  ptrecube  36955  poimirlem16  36971  poimirlem17  36972  poimirlem29  36984  broucube  36989  opnmbllem0  36991  mblfinlem2  36993  mblfinlem3  36994  ismblfin  36996  itg2addnclem  37006  itg2addnclem2  37007  itg2addnclem3  37008  itg2addnc  37009  ibladdnclem  37011  ftc1cnnclem  37026  ftc1cnnc  37027  ftc1anc  37036  geomcau  37094  prdsbnd  37128  cntotbnd  37131  heiborlem4  37149  rrndstprj2  37166  rrncmslem  37167  rrnequiv  37170  iccbnd  37175  cvlcvr1  38676  cvrat3  38780  dalem25  39036  cdlema1N  39129  dalawlem3  39211  dalawlem4  39212  dalawlem5  39213  dalawlem6  39214  dalawlem7  39215  dalawlem9  39217  dalawlem11  39219  dalawlem12  39220  lhp2lt  39339  lhpmcvr  39361  4atexlemcnd  39410  lautj  39431  trlle  39522  trlval3  39525  trlval4  39526  cdleme0moN  39563  cdleme13  39610  cdleme15  39616  cdleme19b  39642  cdleme20e  39651  cdleme20j  39656  cdleme22e  39682  cdleme22eALTN  39683  cdleme26fALTN  39700  cdleme26f  39701  cdleme27N  39707  cdleme41sn3a  39771  cdleme46fsvlpq  39843  cdlemeg46vrg  39865  cdlemg4  39955  cdlemg7N  39964  cdlemg9a  39970  cdlemg11b  39980  cdlemg12a  39981  trljco  40078  tendoidcl  40107  tendococl  40110  tendopltp  40118  tendo0tp  40127  tendoicl  40134  cdlemi2  40157  cdlemk5a  40173  cdlemk5  40174  cdlemk12  40188  cdlemkole  40191  cdlemk14  40192  cdlemk12u  40210  cdlemk37  40252  cdlemk39s-id  40278  cdlemk49  40289  cdlemk39u1  40305  cdlemk39u  40306  dian0  40377  cdlemm10N  40456  cdlemn2  40533  cdlemn10  40544  dihord1  40556  dihord10  40561  dihmeetlem4preN  40644  dihmeetlem18N  40662  dihmeetlem20N  40664  dihjatc  40755  mapdcnvatN  41004  lcmineqlem17  41380  3lexlogpow5ineq2  41390  3lexlogpow2ineq2  41394  3lexlogpow5ineq5  41395  aks4d1p1p3  41404  aks4d1p1p2  41405  aks4d1p1p4  41406  aks4d1p1p7  41409  aks4d1p1p5  41410  aks4d1p1  41411  aks4d1p3  41413  aks4d1p5  41415  aks4d1p6  41416  aks4d1p7d1  41417  aks4d1p7  41418  aks4d1p8  41422  2ap1caineq  41431  sticksstones7  41438  sticksstones10  41441  sticksstones11  41442  sticksstones12a  41443  sticksstones12  41444  sticksstones22  41454  metakunt16  41470  metakunt29  41483  evlselv  41625  fltltc  41869  lzenom  41974  irrapxlem2  42027  irrapxlem3  42028  irrapxlem5  42030  pellexlem2  42034  pell14qrgt0  42063  pellfundlb  42088  pellfundex  42090  pellfund14  42102  rmspecsqrtnq  42110  jm2.24nn  42164  jm2.17a  42165  jm2.17b  42166  congabseq  42179  acongrep  42185  acongeq  42188  jm2.26lem3  42206  jm2.27a  42210  jm2.27c  42212  hbtlem2  42332  dgraaub  42356  idomodle  42404  safesnsupfidom1o  42634  sqrtcval  42858  relexpxpmin  42934  frege102d  42971  hashnzfzclim  43547  binomcxplemfrat  43576  binomcxplemnotnn0  43581  suprnmpt  44335  mpct  44362  rnmptbddlem  44410  dstregt0  44453  lefldiveq  44464  fzisoeu  44472  upbdrech  44477  ssfiunibd  44481  fzdifsuc2  44482  xadd0ge  44492  supxrgere  44505  supxrge  44510  suplesup  44511  xrlexaddrp  44524  infxrunb2  44540  infleinflem2  44543  reclt0d  44559  infrpgernmpt  44637  rexanuz2nf  44665  ioondisj2  44668  iccshift  44693  iooshift  44697  fmul01  44758  fmul01lt1lem1  44762  fmul01lt1lem2  44763  climrec  44781  climsuse  44786  mullimc  44794  mullimcf  44801  constlimc  44802  idlimc  44804  divcnvg  44805  limcperiod  44806  limcrecl  44807  lptioo2  44809  lptioo1  44810  islpcn  44817  lptre2pt  44818  limcleqr  44822  neglimc  44825  addlimc  44826  0ellimcdiv  44827  limclner  44829  climleltrp  44854  limsuplesup  44877  limsupmnflem  44898  supcnvlimsupmpt  44919  0cnv  44920  xlimconst  45003  xlimliminflimsup  45040  sinaover2ne0  45046  cncfshift  45052  cncfperiod  45057  cncfioobdlem  45074  cncfioobd  45075  fperdvper  45097  dvdivbd  45101  dvbdfbdioolem1  45106  dvbdfbdioolem2  45107  ioodvbdlimc1lem1  45109  ioodvbdlimc1lem2  45110  ioodvbdlimc2lem  45112  dvnmul  45121  dvnprodlem1  45124  itgiccshift  45158  itgperiod  45159  ismbl3  45164  ovolsplit  45166  stoweidlem1  45179  stoweidlem11  45189  stoweidlem13  45191  stoweidlem14  45192  stoweidlem16  45194  stoweidlem21  45199  stoweidlem25  45203  stoweidlem26  45204  stoweidlem36  45214  stoweidlem38  45216  stoweidlem41  45219  stoweidlem42  45220  stoweidlem45  45223  stoweidlem48  45226  stoweidlem52  45230  stoweidlem62  45240  wallispilem3  45245  stirlinglem5  45256  stirlinglem6  45257  stirlinglem7  45258  stirlinglem10  45261  stirlinglem12  45263  stirlinglem15  45266  dirkercncflem1  45281  fourierdlem10  45295  fourierdlem12  45297  fourierdlem15  45300  fourierdlem16  45301  fourierdlem19  45304  fourierdlem20  45305  fourierdlem21  45306  fourierdlem22  45307  fourierdlem24  45309  fourierdlem30  45315  fourierdlem37  45322  fourierdlem39  45324  fourierdlem40  45325  fourierdlem41  45326  fourierdlem42  45327  fourierdlem47  45331  fourierdlem48  45332  fourierdlem49  45333  fourierdlem50  45334  fourierdlem52  45336  fourierdlem54  45338  fourierdlem60  45344  fourierdlem61  45345  fourierdlem63  45347  fourierdlem64  45348  fourierdlem68  45352  fourierdlem71  45355  fourierdlem72  45356  fourierdlem73  45357  fourierdlem74  45358  fourierdlem75  45359  fourierdlem76  45360  fourierdlem77  45361  fourierdlem78  45362  fourierdlem79  45363  fourierdlem81  45365  fourierdlem82  45366  fourierdlem83  45367  fourierdlem84  45368  fourierdlem87  45371  fourierdlem92  45376  fourierdlem93  45377  fourierdlem94  45378  fourierdlem101  45385  fourierdlem102  45386  fourierdlem103  45387  fourierdlem104  45388  fourierdlem111  45395  fourierdlem112  45396  fourierdlem113  45397  fourierdlem114  45398  sqwvfoura  45406  sqwvfourb  45407  fouriersw  45409  elaa2lem  45411  etransclem23  45435  etransclem28  45440  etransclem32  45444  etransclem35  45447  etransclem48  45460  qndenserrnbllem  45472  rrnprjdstle  45479  ioorrnopnlem  45482  ioorrnopnxrlem  45484  salexct  45512  sge0fsum  45565  sge0supre  45567  sge0rnbnd  45571  sge0lefi  45576  sge0lessmpt  45577  sge0ltfirp  45578  sge0prle  45579  sge0resrnlem  45581  sge0le  45585  sge0split  45587  sge0iunmptlemre  45593  sge0iunmpt  45596  sge0isum  45605  sge0xaddlem1  45611  sge0xaddlem2  45612  sge0xadd  45613  sge0reuz  45625  sge0reuzb  45626  meaunle  45642  meaiunlelem  45646  voliunsge0lem  45650  meaiuninc  45659  meaiininclem  45664  omeunle  45694  omeiunle  45695  omelesplit  45696  omeiunltfirp  45697  carageniuncllem2  45700  caratheodorylem2  45705  caragencmpl  45713  ovnlecvr  45736  ovncvrrp  45742  ovnsubaddlem1  45748  ovnsubadd  45750  hoidmv1lelem1  45769  hoidmv1lelem2  45770  hoidmv1le  45772  hoidmvlelem1  45773  hoidmvlelem2  45774  hoidmvlelem5  45777  hoidmvle  45778  ovnhoilem1  45779  ovnlecvr2  45788  ovncvr2  45789  hoiqssbllem2  45801  hspmbllem2  45805  hspmbllem3  45806  ovnsplit  45826  ovolval5lem1  45830  vonioolem1  45858  vonioolem2  45859  vonicclem1  45861  vonicclem2  45862  pimconstlt1  45880  smflimlem2  45950  smflimlem4  45952  smfmullem1  45969  smfsuplem1  45989  smflimsuplem4  46001  smflimsuplem5  46002  upwordnul  46056  iccpartltu  46555  iccpartleu  46558  pgrple2abl  47207  difmodm1lt  47373  nnpw2blen  47431  dignn0flhalflem1  47466  2itscp  47632