Theorem eqbrtrd 5061

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

Syntax hints:   → wi 4   = wceq 1543   class class class wbr 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040

This theorem is referenced by:  eqbrtrrd  5063  somin2  5980  en1b  8678  en1bOLD  8679  domunsncan  8723  fodomfi  8927  infsupprpr  9098  hartogslem1  9136  wemaplem2  9141  infdifsn  9250  carddomi2  9551  djuinf  9767  carden  10130  alephsuc3  10159  fpwwe2lem5  10214  fpwwe2lem6  10215  inar1  10354  rankcf  10356  lesub3d  11415  lbinfle  11752  supadd  11765  supmul  11769  rpnnen1lem3  12540  divge1  12619  xrmin1  12732  xrmin2  12733  ifle  12752  qbtwnxr  12755  xltnegi  12771  xleadd1a  12808  xlt2add  12815  xlemul1a  12843  xov1plusxeqvd  13051  ubmelm1fzo  13303  flflp1  13347  ceim1l  13385  ceilm1lt  13386  ceille  13388  quoremz  13393  quoremnn0ALT  13395  modlt  13418  modeqmodmin  13479  addmodlteq  13484  seqf1olem1  13580  bernneq  13761  discr  13772  faclbnd2  13822  faclbnd4lem3  13826  hashun2  13915  hashfun  13969  ccatsymb  14104  ccatrn  14111  sqrlem6  14776  sqrlem7  14777  rddif  14869  amgm2  14898  icodiamlt  14964  climconst  15069  rlimconst  15070  serclim0  15103  rlimcn1  15114  mulcn2  15122  reccn2  15123  o1mul  15141  o1rlimmul  15145  iserex  15185  climlec2  15187  iserge0  15189  climcau  15199  caucvgrlem  15201  caucvgr  15204  iseraltlem2  15211  iseraltlem3  15212  iseralt  15213  fsumabs  15328  o1fsum  15340  iserabs  15342  climfsum  15347  isumless  15372  climcndslem2  15377  divrcnv  15379  flo1  15381  supcvg  15383  georeclim  15399  geomulcvg  15403  cvgrat  15410  mertenslem1  15411  prodfclim1  15420  fprodle  15521  efcvgfsum  15610  eftlub  15633  eflegeo  15645  tanhlt1  15684  tanhbnd  15685  ef01bndlem  15708  sin01bnd  15709  cos01bnd  15710  cos01gt0  15715  ruclem2  15756  ruclem3  15757  ruclem9  15762  ruclem11  15764  ruclem12  15765  bitsfzolem  15956  bitsfzo  15957  bitsinv1lem  15963  sadcaddlem  15979  mulgcd  16071  eucalglt  16105  lcmledvds  16119  lcmfledvds  16152  mulgcddvds  16175  coprmproddvdslem  16182  prmind2  16205  isprm5  16227  divdenle  16268  nonsq  16278  pythagtriplem4  16335  pclem  16354  pcpremul  16359  pczdvds  16379  pcprmpw2  16398  qexpz  16417  prmreclem4  16435  prmreclem5  16436  4sqlem10  16463  ramtub  16528  ramub2  16530  prmodvdslcmf  16563  prmgaplem8  16574  natpropd  17439  catciso  17571  p0le  17889  acsdomd  18017  triv1nsgd  18543  qusgrp  18553  f1otrspeq  18793  pmtrfrn  18804  pmtrfconj  18812  symggen  18816  psgnunilem4  18843  oddvds2  18911  odcau  18947  pgpfi  18948  pgpssslw  18957  sylow3lem4  18973  efgred2  19097  frgp0  19104  odadd2  19188  oddvdssubg  19194  ablfac1c  19412  ablfac1eu  19414  pgpfaclem3  19424  2nsgsimpgd  19443  isabvd  19810  abvsubtri  19825  cyggic  20491  mplsubrg  20921  coe1sfi  21088  mp2pm2mplem5  21661  en2top  21836  1stcrest  22304  2ndcrest  22305  hausmapdom  22351  ufilen  22781  xmetrtri2  23208  prdsxmetlem  23220  bl2in  23252  xblcntrps  23262  xblcntr  23263  ssblps  23274  ssbl  23275  blssps  23276  blss  23277  blcld  23357  methaus  23372  metustexhalf  23408  nmtri2  23479  tngngp3  23508  nrginvrcnlem  23543  nrginvrcn  23544  nmoi  23580  nmo0  23587  nmoid  23594  blcvx  23649  reperflem  23669  reconnlem2  23678  metdcnlem  23687  metdscn  23707  metnrmlem3  23712  mulc1cncf  23756  iccpnfhmeo  23796  cnheiborlem  23805  cnheibor  23806  lebnumii  23817  pcopt  23873  pcopt2  23874  pcoass  23875  nmoleub2lem  23965  nmoleub2lem3  23966  nmoleub2lem2  23967  ipcau2  24085  tcphcphlem1  24086  nglmle  24153  trirn  24251  rrxdstprj1  24260  minveclem3  24280  ivthlem2  24303  ivthlem3  24304  ivth2  24306  ovollb  24330  ovolsslem  24335  ovollb2lem  24339  ovolctb  24341  ovoliunlem1  24353  ovolsca  24366  ovolicc1  24367  ovolicc2lem4  24371  nulmbl  24386  ioombl1lem4  24412  uniioovol  24430  uniioombllem3a  24435  uniioombllem4  24437  opnmbllem  24452  volcn  24457  volivth  24458  i1fadd  24546  i1fmul  24547  mbfi1fseqlem4  24570  mbfi1fseqlem5  24571  mbfi1fseqlem6  24572  itg2const2  24593  itg2seq  24594  itg2uba  24595  itg2split  24601  itg2monolem1  24602  itg2monolem3  24604  itg2i1fseq2  24608  itg2addlem  24610  itg2gt0  24612  itg2cnlem1  24613  itg2cnlem2  24614  itgless  24668  ibladdlem  24671  bddmulibl  24690  dveflem  24830  dvferm1lem  24835  dvferm2lem  24837  dvlip  24844  dvlipcn  24845  dvlip2  24846  dvle  24858  dvivthlem1  24859  lhop1lem  24864  dvcvx  24871  dvfsumabs  24874  dvfsumlem2  24878  dvfsumlem4  24880  dvfsumrlim2  24883  dvfsum2  24885  ftc1a  24888  ftc1lem4  24890  ftc1lem5  24891  deg1sub  24960  ply1divex  24988  deg1submon1p  25004  r1pdeglt  25010  dvdsq1p  25012  fta1glem2  25018  fta1g  25019  plyeq0lem  25058  dgrlt  25114  fta1lem  25154  aalioulem2  25180  aalioulem3  25181  aalioulem4  25182  aaliou3lem2  25190  aaliou3lem9  25197  taylply2  25214  ulmbdd  25244  ulmdvlem1  25246  mtest  25250  mtestbdd  25251  radcnvlem1  25259  radcnvle  25266  pserulm  25268  psercn  25272  pserdvlem2  25274  abelthlem2  25278  abelthlem5  25281  abelthlem7  25284  abelthlem8  25285  abelthlem9  25286  reeff1olem  25292  tangtx  25349  tanord  25381  efif1olem4  25388  logrnaddcl  25417  logcj  25448  logimul  25456  logneg2  25457  logdivlti  25462  divlogrlim  25477  logcnlem3  25486  logcnlem4  25487  efopn  25500  logtayllem  25501  logtayl  25502  cxpcn3lem  25587  cxpaddle  25592  abscxpbnd  25593  asinlem3  25708  asinneg  25723  asinsin  25729  atanlogaddlem  25750  atantan  25760  bndatandm  25766  atans2  25768  atantayl  25774  atantayl2  25775  atantayl3  25776  leibpi  25779  birthdaylem3  25790  rlimcnp  25802  efrlim  25806  cxplim  25808  cxp2lim  25813  cxploglim2  25815  divsqrtsumo1  25820  jensenlem2  25824  amgm  25827  logdifbnd  25830  harmonicbnd4  25847  fsumharmonic  25848  lgamgulmlem2  25866  lgamgulmlem3  25867  lgamgulmlem5  25869  lgambdd  25873  lgamcvg2  25891  ftalem1  25909  ftalem5  25913  basellem1  25917  basellem8  25924  ppip1le  25997  ppiltx  26013  sqff1o  26018  chtublem  26046  chpub  26055  logfaclbnd  26057  logfacrlim  26059  logexprlim  26060  mersenne  26062  bcmono  26112  bcmax  26113  bposlem2  26120  bposlem5  26123  lgslem3  26134  gausslemma2dlem1a  26200  lgsquadlem1  26215  lgsquadlem2  26216  2lgslem1c  26228  2sqblem  26266  chebbnd1  26307  chtppilimlem1  26308  chto1ub  26311  chpchtlim  26314  chpo1ubb  26316  rplogsumlem1  26319  rplogsumlem2  26320  rpvmasumlem  26322  dchrisumlem1  26324  dchrisumlem2  26325  dchrmusum2  26329  dchrvmasumlem2  26333  dchrvmasumlem3  26334  dchrvmasumiflem1  26336  dchrisum0flblem1  26343  dchrisum0fno1  26346  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem2a  26352  dchrisum0lem2  26353  rplogsum  26362  mudivsum  26365  mulogsumlem  26366  mulog2sumlem1  26369  mulog2sumlem2  26370  vmalogdivsum2  26373  2vmadivsumlem  26375  selberglem2  26381  selberg2b  26387  logdivbnd  26391  selberg3lem1  26392  selberg3lem2  26393  selberg4lem1  26395  pntrmax  26399  pntrsumo1  26400  pntrlog2bndlem1  26412  pntrlog2bndlem2  26413  pntrlog2bndlem3  26414  pntrlog2bndlem4  26415  pntrlog2bndlem5  26416  pntrlog2bnd  26419  pntpbnd1a  26420  pntpbnd2  26422  pntibndlem2  26426  pntlemb  26432  pntlemg  26433  pntlemh  26434  pntlemr  26437  pntlemj  26438  pntlemf  26440  pntlemo  26442  pnt  26449  padicabv  26465  ostth2lem2  26469  ostth2lem3  26470  ostth3  26473  colperpexlem3  26777  mideulem2  26779  lnperpex  26848  trgcopy  26849  iscgra1  26855  brbtwn2  26950  colinearalglem4  26954  subupgr  27329  crctcshwlkn0lem1  27848  nvabs  28707  nvge0  28708  smcnlem  28732  nmblolbii  28834  blocnilem  28839  siii  28888  ubthlem2  28906  minvecolem3  28911  htthlem  28952  bcsiALT  29214  bcs3  29218  chscllem4  29675  0cnop  30014  0cnfn  30015  nmbdoplbi  30059  nmcoplbi  30063  nmophmi  30066  nmbdfnlbi  30084  nmcfnlbi  30087  nlelchi  30096  riesz1  30100  cnlnadjlem2  30103  nmopadjlei  30123  nmoptrii  30129  nmopcoi  30130  nmopcoadji  30136  unierri  30139  branmfn  30140  pjs14i  30245  hstle  30265  cdj3lem2b  30472  xlt2addrd  30755  eliccelico  30772  elicoelioo  30773  ltesubnnd  30810  wrdt2ind  30899  archirngz  31116  archiabllem2c  31122  madjusmdetlem2  31446  locfinref  31459  sqsscirc1  31526  tpr2rico  31530  esumcst  31697  esumgect  31724  esum2d  31727  measunl  31850  measiun  31852  omssubaddlem  31932  omssubadd  31933  carsgsigalem  31948  carsgclctunlem2  31952  pmeasmono  31957  eulerpartlemgc  31995  eulerpartlemb  32001  ballotlemsel1i  32145  ballotlemro  32155  sgnsub  32177  signsplypnf  32195  signsply0  32196  signsvtn  32229  signsvfnn  32231  hgt750lemd  32294  logdivsqrle  32296  hashf1dmcdm  32743  erdsze2lem1  32832  sinccvglem  33297  divcnvlin  33367  iprodefisum  33376  faclimlem2  33379  nosep1o  33570  nodense  33581  noinfbnd2lem1  33619  noetainflem3  33628  cofcutr  33778  cofcutrtime  33779  fnemeet1  34241  dnibndlem10  34353  dnibndlem11  34354  dnibnd  34357  knoppcnlem4  34362  knoppcnlem6  34364  unblimceq0lem  34372  unbdqndv2lem1  34375  unbdqndv2lem2  34376  knoppndvlem11  34388  knoppndvlem12  34389  knoppndvlem14  34391  knoppndvlem15  34392  knoppndvlem17  34394  knoppndvlem18  34395  knoppndvlem19  34396  knoppndvlem21  34398  ctbssinf  35263  ltflcei  35451  ptrecube  35463  poimirlem16  35479  poimirlem17  35480  poimirlem29  35492  broucube  35497  opnmbllem0  35499  mblfinlem2  35501  mblfinlem3  35502  ismblfin  35504  itg2addnclem  35514  itg2addnclem2  35515  itg2addnclem3  35516  itg2addnc  35517  ibladdnclem  35519  ftc1cnnclem  35534  ftc1cnnc  35535  ftc1anc  35544  geomcau  35603  prdsbnd  35637  cntotbnd  35640  heiborlem4  35658  rrndstprj2  35675  rrncmslem  35676  rrnequiv  35679  iccbnd  35684  cvlcvr1  37039  cvrat3  37142  dalem25  37398  cdlema1N  37491  dalawlem3  37573  dalawlem4  37574  dalawlem5  37575  dalawlem6  37576  dalawlem7  37577  dalawlem9  37579  dalawlem11  37581  dalawlem12  37582  lhp2lt  37701  lhpmcvr  37723  4atexlemcnd  37772  lautj  37793  trlle  37884  trlval3  37887  trlval4  37888  cdleme0moN  37925  cdleme13  37972  cdleme15  37978  cdleme19b  38004  cdleme20e  38013  cdleme20j  38018  cdleme22e  38044  cdleme22eALTN  38045  cdleme26fALTN  38062  cdleme26f  38063  cdleme27N  38069  cdleme41sn3a  38133  cdleme46fsvlpq  38205  cdlemeg46vrg  38227  cdlemg4  38317  cdlemg7N  38326  cdlemg9a  38332  cdlemg11b  38342  cdlemg12a  38343  trljco  38440  tendoidcl  38469  tendococl  38472  tendopltp  38480  tendo0tp  38489  tendoicl  38496  cdlemi2  38519  cdlemk5a  38535  cdlemk5  38536  cdlemk12  38550  cdlemkole  38553  cdlemk14  38554  cdlemk12u  38572  cdlemk37  38614  cdlemk39s-id  38640  cdlemk49  38651  cdlemk39u1  38667  cdlemk39u  38668  dian0  38739  cdlemm10N  38818  cdlemn2  38895  cdlemn10  38906  dihord1  38918  dihord10  38923  dihmeetlem4preN  39006  dihmeetlem18N  39024  dihmeetlem20N  39026  dihjatc  39117  mapdcnvatN  39366  lcmineqlem17  39736  3lexlogpow5ineq2  39746  3lexlogpow2ineq2  39750  3lexlogpow5ineq5  39751  aks4d1p1p3  39759  aks4d1p1p2  39760  aks4d1p1p4  39761  aks4d1p1p7  39764  aks4d1p1p5  39765  aks4d1p1  39766  2ap1caineq  39770  sticksstones7  39777  sticksstones10  39780  sticksstones11  39781  sticksstones12a  39782  sticksstones12  39783  metakunt16  39803  metakunt29  39816  fltltc  40142  lzenom  40236  irrapxlem2  40289  irrapxlem3  40290  irrapxlem5  40292  pellexlem2  40296  pell14qrgt0  40325  pellfundlb  40350  pellfundex  40352  pellfund14  40364  rmspecsqrtnq  40372  jm2.24nn  40425  jm2.17a  40426  jm2.17b  40427  congabseq  40440  acongrep  40446  acongeq  40449  jm2.26lem3  40467  jm2.27a  40471  jm2.27c  40473  hbtlem2  40593  dgraaub  40617  idomodle  40665  sqrtcval  40866  relexpxpmin  40943  frege102d  40980  hashnzfzclim  41554  binomcxplemfrat  41583  binomcxplemnotnn0  41588  suprnmpt  42324  mpct  42355  rnmptbddlem  42402  dstregt0  42433  lefldiveq  42445  fzisoeu  42453  upbdrech  42458  ssfiunibd  42462  fzdifsuc2  42463  xadd0ge  42473  supxrgere  42486  supxrge  42491  suplesup  42492  xrlexaddrp  42505  infxrunb2  42521  infleinflem2  42524  reclt0d  42540  infrpgernmpt  42621  ioondisj2  42647  iccshift  42672  iooshift  42676  fmul01  42739  fmul01lt1lem1  42743  fmul01lt1lem2  42744  climrec  42762  climsuse  42767  mullimc  42775  mullimcf  42782  constlimc  42783  idlimc  42785  divcnvg  42786  limcperiod  42787  limcrecl  42788  lptioo2  42790  lptioo1  42791  islpcn  42798  lptre2pt  42799  limcleqr  42803  neglimc  42806  addlimc  42807  0ellimcdiv  42808  limclner  42810  climleltrp  42835  limsuplesup  42858  limsupmnflem  42879  supcnvlimsupmpt  42900  0cnv  42901  xlimconst  42984  xlimliminflimsup  43021  sinaover2ne0  43027  cncfshift  43033  cncfperiod  43038  cncfioobdlem  43055  cncfioobd  43056  fperdvper  43078  dvdivbd  43082  dvbdfbdioolem1  43087  dvbdfbdioolem2  43088  ioodvbdlimc1lem1  43090  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvnmul  43102  dvnprodlem1  43105  itgiccshift  43139  itgperiod  43140  ismbl3  43145  ovolsplit  43147  stoweidlem1  43160  stoweidlem11  43170  stoweidlem13  43172  stoweidlem14  43173  stoweidlem16  43175  stoweidlem21  43180  stoweidlem25  43184  stoweidlem26  43185  stoweidlem36  43195  stoweidlem38  43197  stoweidlem41  43200  stoweidlem42  43201  stoweidlem45  43204  stoweidlem48  43207  stoweidlem52  43211  stoweidlem62  43221  wallispilem3  43226  stirlinglem5  43237  stirlinglem6  43238  stirlinglem7  43239  stirlinglem10  43242  stirlinglem12  43244  stirlinglem15  43247  dirkercncflem1  43262  fourierdlem10  43276  fourierdlem12  43278  fourierdlem15  43281  fourierdlem16  43282  fourierdlem19  43285  fourierdlem20  43286  fourierdlem21  43287  fourierdlem22  43288  fourierdlem24  43290  fourierdlem30  43296  fourierdlem37  43303  fourierdlem39  43305  fourierdlem40  43306  fourierdlem41  43307  fourierdlem42  43308  fourierdlem47  43312  fourierdlem48  43313  fourierdlem49  43314  fourierdlem50  43315  fourierdlem52  43317  fourierdlem54  43319  fourierdlem60  43325  fourierdlem61  43326  fourierdlem63  43328  fourierdlem64  43329  fourierdlem68  43333  fourierdlem71  43336  fourierdlem72  43337  fourierdlem73  43338  fourierdlem74  43339  fourierdlem75  43340  fourierdlem76  43341  fourierdlem77  43342  fourierdlem78  43343  fourierdlem79  43344  fourierdlem81  43346  fourierdlem82  43347  fourierdlem83  43348  fourierdlem84  43349  fourierdlem87  43352  fourierdlem92  43357  fourierdlem93  43358  fourierdlem94  43359  fourierdlem101  43366  fourierdlem102  43367  fourierdlem103  43368  fourierdlem104  43369  fourierdlem111  43376  fourierdlem112  43377  fourierdlem113  43378  fourierdlem114  43379  sqwvfoura  43387  sqwvfourb  43388  fouriersw  43390  elaa2lem  43392  etransclem23  43416  etransclem28  43421  etransclem32  43425  etransclem35  43428  etransclem48  43441  qndenserrnbllem  43453  rrnprjdstle  43460  ioorrnopnlem  43463  ioorrnopnxrlem  43465  salexct  43491  sge0fsum  43543  sge0supre  43545  sge0rnbnd  43549  sge0lefi  43554  sge0lessmpt  43555  sge0ltfirp  43556  sge0prle  43557  sge0resrnlem  43559  sge0le  43563  sge0split  43565  sge0iunmptlemre  43571  sge0iunmpt  43574  sge0isum  43583  sge0xaddlem1  43589  sge0xaddlem2  43590  sge0xadd  43591  sge0reuz  43603  sge0reuzb  43604  meaunle  43620  meaiunlelem  43624  voliunsge0lem  43628  meaiuninc  43637  meaiininclem  43642  omeunle  43672  omeiunle  43673  omelesplit  43674  omeiunltfirp  43675  carageniuncllem2  43678  caratheodorylem2  43683  caragencmpl  43691  ovnlecvr  43714  ovncvrrp  43720  ovnsubaddlem1  43726  ovnsubadd  43728  hoidmv1lelem1  43747  hoidmv1lelem2  43748  hoidmv1le  43750  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem5  43755  hoidmvle  43756  ovnhoilem1  43757  ovnlecvr2  43766  ovncvr2  43767  hoiqssbllem2  43779  hspmbllem2  43783  hspmbllem3  43784  ovnsplit  43804  ovolval5lem1  43808  vonioolem1  43836  vonioolem2  43837  vonicclem1  43839  vonicclem2  43840  pimconstlt1  43857  smflimlem2  43922  smflimlem4  43924  smfmullem1  43940  smfsuplem1  43959  smflimsuplem4  43971  smflimsuplem5  43972  iccpartltu  44493  iccpartleu  44496  pgrple2abl  45317  difmodm1lt  45484  nnpw2blen  45542  dignn0flhalflem1  45577  2itscp  45743