Theorem breqtrrd 5136

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

Hypotheses

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

Assertion

Ref	Expression
breqtrrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrd

Step	Hyp	Ref	Expression
1		breqtrrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2769	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrd 5134	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  marypha1lem  9449  marypha2  9455  infsupprpr  9522  unxpwdom  9607  ttrcltr  9741  onadju  10296  nnadju  10300  cfss  10367  tskuni  10892  ltexnq  11084  lt2addmuld  12620  div4p1lem1div2  12625  nn0le2x  12684  mul2lt0rgt0  13249  prodge0ld  13254  ge2halflem1  13261  xrmax1  13329  xrmax2  13330  max1ALT  13340  qbtwnxr  13354  xleadd1a  13407  xlt2add  13414  xlesubadd  13417  xmulgt0  13437  xlemul1a  13442  xov1plusxeqvd  13653  uzsubsubfz  13704  subfzo0  13952  flflp1  13971  ceilge  14009  modge0  14043  modlt  14044  modid  14060  m1modge3gt1  14085  modaddmodup  14101  sermono  14201  seqf1olem1  14208  seqf1olem2  14209  sqgt0  14293  sqge0  14303  leexp1a  14342  nnlesq  14373  expnbnd  14400  expmulnbnd  14403  discr1  14407  facwordi  14457  faclbnd5  14466  nfile  14527  hashdom  14547  hashgt23el  14593  fi1uzind  14676  brfi1indALT  14679  ccatdmss  14751  ccatws1n0  14805  swrds2  15117  sgnmul  15286  cjmulge0  15339  resqrtcl  15446  absge0  15480  sqreulem  15553  amgm2  15563  rlimdm  15744  rlimge0  15774  reccn2  15790  climle  15833  climserle  15856  isercoll2  15862  iseraltlem1  15875  iseralt  15878  isumclim2  15950  isumclim3  15951  isumge0  15958  fsumless  15989  cvgcmp  16009  cvgcmpce  16011  abscvgcvg  16012  isumsup2  16041  isumltss  16043  climcndslem1  16044  climcnds  16046  supcvg  16051  harmonic  16054  expcnv  16059  explecnv  16060  cvgrat  16078  mertenslem1  16079  mertenslem2  16080  clim2div  16084  ntrivcvgtail  16095  iprodclim2  16192  iprodclim3  16193  efcvg  16277  ege2le3  16282  efaddlem  16285  eftlub  16303  effsumlt  16305  tanhlt1  16354  ef01bndlem  16378  sin02gt0  16386  rpnnen2lem4  16411  ruclem2  16426  ruclem3  16427  ruclem9  16432  iddvdsexp  16475  dvdsadd  16498  dvdsfac  16522  dvdsexp2im  16523  dvdsmod  16525  3dvds  16527  omoe  16560  sumeven  16583  divalglem1  16590  flodddiv4t2lthalf  16614  bitsfzo  16631  bitsmod  16632  bitscmp  16634  bitsinv1lem  16637  sadcaddlem  16653  sadadd3  16657  sadaddlem  16662  dvdssqim  16753  dvdsexpim  16754  dvdsmulgcd  16756  nn0seqcvgd  16771  dvdslcm  16799  lcmgcdlem  16807  dvdslcmf  16832  lcmfunsnlem2lem2  16840  mulgcddvds  16856  qredeq  16858  cncongr2  16869  sqnprm  16904  isprm6  16916  dvdszzq  16923  prmdvdsbc  16928  nonsq  16961  hashdvds  16978  prmdiv  16988  odzdvds  16999  pythagtriplem4  17023  pcpre1  17046  pcdvdsb  17073  pcz  17085  pcprmpw2  17086  pcaddlem  17092  pcadd  17093  pcadd2  17094  pcmpt  17096  pcmptdvds  17098  fldivp1  17101  pcfaclem  17102  pockthlem  17109  prmreclem1  17120  prmreclem3  17122  prmreclem5  17124  prmreclem6  17125  4sqlem6  17147  4sqlem8  17149  4sqlem11  17159  4sqlem12  17160  4sqlem14  17162  4sqlem16  17164  vdwlem3  17187  vdwlem9  17193  vdwlem10  17194  vdwlem12  17196  ramub1lem2  17231  prmgap  17263  prmgaplcm  17264  prmgapprmo  17266  mreexexd  17848  invfuc  18178  ple1  18628  chnub  18822  eqgen  19419  lagsubg  19436  pgpfi  19846  sylow2alem2  19859  sylow2a  19860  sylow3lem4  19871  efgsrel  19975  odadd1  20089  odadd2  20090  gexex  20094  lt6abl  20136  dprd2d2  20287  dmdprdpr  20292  ablfacrp2  20310  ablfac1c  20314  pgpfaclem1  20324  ablfac2  20332  fincygsubgodd  20355  omndmul2  20374  dvdsrmul1  20626  unitmulclb  20638  subrguss  20866  rhmsubcrngc  20947  abvres  21115  znfld  21893  znunit  21896  ofldchr  21909  frlmisfrlm  22181  ply1coefsupp  22642  evl1gsumadd  22703  matgsum  22779  pm2mpcl  23142  psmetxrge0  24659  isxmet2d  24673  mettri  24698  xmettri3  24699  mettri3  24700  xmetrtri2  24702  prdsxmetlem  24714  imasdsf1olem  24719  xblss2ps  24747  blss2ps  24749  blss2  24750  blssps  24770  blss  24771  prdsbl  24837  dscmet  24918  nmge0  24963  nmmtri  24968  tngngp3  25002  nlmvscnlem2  25031  nrginvrcnlem  25037  nmoix  25075  nmoleub  25077  blcvx  25144  xrsxmet  25156  opnreen  25178  xrge0tsms  25181  icopnfcnv  25290  xrhmeo  25294  lebnumii  25314  pcophtb  25377  pi1grplem  25397  nmoleub2lem  25462  ipcau2  25582  tcphcphlem1  25583  ipcau  25586  ipcnlem2  25592  rrxcph  25740  minveclem2  25774  minveclem3b  25776  pjthlem1  25785  pjthlem2  25786  ivthlem3  25801  ivth2  25803  ovolfsf  25819  ovolsslem  25832  ovollb2lem  25836  ovollb2  25837  ovolctb  25838  ovolfiniun  25849  ovolicc1  25864  ovolicc2lem4  25868  ovolicc2  25870  nulmbl2  25884  unmbl  25885  ioombl1lem4  25909  uniioombllem4  25934  uniioombllem6  25936  volivth  25955  vitalilem4  25959  itg1ge0  26034  itg1ge0a  26059  itg1lea  26060  itg1climres  26062  mbfi1fseqlem5  26067  itg2ub  26081  itg2seq  26090  itg2uba  26091  itg2splitlem  26096  itg2split  26097  itg2monolem3  26100  itg2mono  26101  itg2i1fseq2  26104  itg2addlem  26106  iblss  26152  itggt0  26191  dvferm2lem  26333  dvlip  26340  dvivthlem1  26355  dvfsumlem2  26374  dvfsumlem3  26375  ftc1lem4  26386  ply1divmo  26481  ply1remlem  26510  fta1glem2  26514  idomrootle  26518  ig1pdvds  26525  plyeq0lem  26556  plydiveu  26646  fta1lem  26655  vieta1lem2  26661  aaliou3lem2  26697  aaliou3lem8  26699  ulmcn  26753  mtest  26758  itgulm  26762  radcnvlem1  26767  radcnvlt1  26772  dvradcnv  26775  pserdvlem2  26782  abelthlem2  26786  abelthlem6  26790  abelthlem7  26792  abelthlem9  26794  tangtx  26861  sinq12gt0  26863  sineq0  26879  cosordlem  26885  tanord  26893  tanregt0  26894  logrnaddcl  26929  logcj  26961  argregt0  26965  argrege0  26966  argimgt0  26967  argimlt0  26968  logimul  26969  logneg2  26970  logdivlti  26975  divlogrlim  26990  logcnlem3  26999  logcnlem4  27000  dvlog2lem  27007  logtayl  27015  rpcxpcl  27031  cxpsqrtlem  27057  cxpaddle  27107  isosctrlem1  27173  asinlem3a  27225  asinlem3  27226  asinneg  27241  asinsinlem  27246  asinsin  27247  atanlogaddlem  27268  atanlogadd  27269  atanlogsublem  27270  atanlogsub  27271  atantan  27278  atanbndlem  27280  atantayl  27292  leibpi  27297  birthdaylem3  27308  areaf  27316  cxploglim  27332  jensenlem2  27342  jensen  27343  logdiflbnd  27349  harmonicbnd4  27365  fsumharmonic  27366  zetacvg  27369  lgamgulmlem2  27384  lgamgulmlem3  27385  lgamcvg2  27409  wilthlem2  27423  wilthimp  27426  ftalem1  27427  ftalem2  27428  ftalem5  27431  basellem6  27440  basellem8  27442  basellem9  27443  chtge0  27466  chtublem  27565  logexprlim  27579  perfectlem1  27583  bcmax  27632  bposlem1  27638  bposlem2  27639  bposlem6  27643  bposlem7  27644  lgsdilem2  27687  lgsqrlem4  27703  lgsquadlem1  27734  2lgsoddprmlem2  27763  2sqlem3  27774  2sqlem8  27780  2sqblem  27785  2sqmod  27790  chebbnd1lem2  27824  chtppilimlem1  27827  chtppilim  27829  chto1ub  27830  vmadivsum  27836  rplogsumlem1  27838  rplogsumlem2  27839  dchrisum0lem1a  27840  rpvmasumlem  27841  dchrisumlem1  27843  dchrisumlem2  27844  dchrvmasumlem2  27852  dchrisum0flblem1  27862  dchrisum0flblem2  27863  dchrisum0lem1b  27869  dchrisum0lem1  27870  dchrisum0lem2a  27871  dchrisum0lem3  27873  dchrisum0  27874  mudivsum  27884  mulogsumlem  27885  mulog2sumlem1  27888  mulog2sumlem2  27889  2vmadivsumlem  27894  chpdifbndlem1  27907  selberg3lem1  27911  selberg4lem1  27914  pntrlog2bndlem1  27931  pntrlog2bndlem2  27932  pntrlog2bndlem3  27933  pntrlog2bndlem4  27934  pntpbnd1a  27939  pntpbnd1  27940  pntpbnd2  27941  pntibndlem2  27945  pntibndlem3  27946  pntlemd  27948  pntlemc  27949  pntlemb  27951  pntlemg  27952  pntlemh  27953  pntlemr  27956  pntlemf  27959  pntlemo  27961  abvcxp  27969  ostth2lem1  27972  padicabv  27984  ostth2lem2  27988  ostth2lem3  27989  ostth2lem4  27990  ostth2  27991  ostth3  27992  flt4lem5  28007  nodense  28076  nogt01o  28080  nosupbnd2lem1  28099  noetasuplem3  28119  maxs1  28153  maxs2  28154  eqcuts3  28217  cofcutr  28337  cofcutrtime  28340  addsuniflem  28414  negsunif  28468  sltmuls2  28561  precsexlem11  28630  abssge0  28658  leabss  28661  oncutlt  28677  om2noseqlt  28712  zsoring  28822  expsgt0  28850  halfcut  28871  addhalfcut  28872  bdayfinbndlem1  28880  elreno2  28908  tgcgr4  29021  legso  29089  krippenlem  29189  midex  29240  oppperpex  29256  angmgmaddcpbl  29417  angmgmaddlid  29419  angmgmaddrid  29420  prlngmid2  29466  prlngsymquadopp  29470  quadcgrprlng  29471  ttgcontlem1  29489  axpaschlem  29545  axcontlem8  29576  upgrex  29697  nbfusgrlevtxm1  29985  finsumvtxdgeven  30160  swrdwlk  30295  wwlksnextproplem3  30527  clwlkclwwlk2  30621  clwlkclwwlkfolem  30625  clwwlkndivn  30698  ex-ind-dvds  31089  nvabs  31301  nmooge0  31396  nmoolb  31400  siii  31482  minvecolem2  31504  minvecolem4  31509  minvecolem5  31510  hlipgt0  31543  normge0  31755  normpyc  31775  pjhthlem1  32020  pjige0i  32319  nmoplb  32536  nmfnlb  32553  branmfn  32734  pjssdif2i  32803  stlei  32869  xlt2addrd  33418  eliccelico  33436  elicoelioo  33437  bcm1n  33454  fsumiunle  33487  nexple  33491  expevenpos  33493  pfxlsw2ccat  33580  wrdt2ind  33583  xrge0tsmsd  33701  gsumwrd2dccatlem  33705  psgnfzto1stlem  33728  cycpmco2lem4  33757  cycpmco2lem5  33758  cyc3conja  33785  archirngz  33817  archiabllem2c  33823  rprmasso2  34125  rprmirred  34130  1arithufdlem3  34145  vietadeg1  34277  lbslelsp  34297  fedgmullem2  34329  extdggt0  34356  evls1fldgencl  34369  fldextrspunlem1  34374  extdgfialglem1  34391  algextdeglem8  34423  rtelextdg2lem  34425  cos9thpiminplylem1  34481  cos9thpiminplylem2  34482  madjusmdetlem2  34527  locfinreflem  34539  xrge0iifiso  34634  gsumesum  34758  esumcst  34762  esumpcvgval  34777  esumcvg  34785  esumiun  34793  measssd  34915  measunl  34916  omssubadd  34999  carsgclctunlem3  35019  pmeasmono  35023  sibfof  35039  oddpwdc  35053  eulerpartlemgc  35061  iwrdsplit  35086  ballotlemsgt1  35210  ballotlemsel1i  35212  signsply0  35247  signstfvc  35270  signsvtp  35279  signsvfpn  35281  fdvposlt  35295  fdvneggt  35296  fdvnegge  35298  logdivsqrle  35346  hgt750lemf  35349  tgoldbachgtde  35356  subfaclim  36119  erdszelem7  36128  erdszelem8  36129  cvmliftlem2  36217  snmlff  36260  sinccvglem  36603  climlec3  36676  faclim  36688  fnejoin1  37333  poimirlem12  38741  poimirlem17  38746  poimirlem19  38748  poimirlem20  38749  poimirlem23  38752  poimirlem28  38757  broucube  38763  mblfinlem2  38767  mblfinlem3  38768  mblfinlem4  38769  ismblfin  38770  itg2addnclem  38780  itg2addnclem3  38782  itg2gt0cn  38784  itggt0cn  38799  ftc1anclem5  38806  ftc1anclem7  38808  ftc1anclem8  38809  isbnd3  38909  ssbnd  38913  heiborlem8  38943  bfplem2  38948  rrncmslem  38957  rrnequiv  38960  rrntotbnd  38961  lcv1  40289  lsatcv0eq  40295  lsatcvat3  40300  cvlsupr2  40591  hlatlej2  40624  cvrval4N  40662  cvratlem  40669  atcvr0eq  40674  2atlt  40687  atbtwnex  40696  athgt  40704  1cvrat  40724  ps-1  40725  hlatexch3N  40728  hlatexch4  40729  3atlem2  40732  atcvrlln2  40767  lplnexllnN  40812  4atlem3a  40845  4atlem10b  40853  4atlem11b  40856  4atlem12b  40859  2lplnja  40867  dalemply  40902  dalemsly  40903  dalem1  40907  dalem6  40916  dalem7  40917  dalem-cly  40919  dalem11  40922  dalem12  40923  dalem16  40927  dalem17  40928  dalem38  40958  dalem44  40964  dalem61  40981  lnatexN  41027  lncvrat  41030  lncmp  41031  paddasslem2  41069  dalawlem3  41121  dalawlem6  41124  dalawlem11  41129  lhpmcvr  41271  lhp2atne  41282  lhp2at0ne  41284  lautj  41341  trlval4  41436  cdlemc2  41440  cdlemc5  41443  cdleme3b  41477  cdleme11c  41509  cdleme19a  41551  cdleme20j  41566  cdleme22f  41594  cdleme23c  41599  cdleme26f2ALTN  41612  cdleme26f2  41613  cdleme35fnpq  41697  cdleme48bw  41750  cdlemg10a  41888  cdlemg11b  41890  cdlemg17g  41915  cdlemg18c  41928  cdlemi1  42066  cdlemk52  42202  dia2dimlem1  42312  dihord1  42466  dihjatcclem4  42669  lcmineqlem15  43284  lcmineqlem19  43288  lcmineqlem22  43291  aks4d1lem1  43303  aks4d1p1p4  43312  aks4d1p1p5  43316  aks4d1p2  43318  aks4d1p3  43319  aks4d1p6  43322  aks4d1p7d1  43323  aks4d1p7  43324  aks4d1p8  43328  aks4d1p9  43329  aks6d1c1p6  43355  aks6d1c1  43357  aks6d1c2  43371  sticksstones7  43393  aks6d1c7lem1  43421  unitscyglem4  43439  dvdsexpnn0  43577  prjspnequivnorm  43851  prjspnnorm  43852  fltnltalem  43864  fltnlta  43865  3cubeslem1  43885  eldioph2lem1  43962  lzenom  43972  irrapxlem1  44020  irrapxlem4  44023  irrapxlem5  44024  pell14qrgt0  44057  pell1qrge1  44068  pell1qrgap  44072  pellfundge  44080  pellfundex  44084  pellfund14  44096  rmspecsqrtnq  44104  rmxypos  44145  ltrmynn0  44146  ltrmxnn0  44147  jm2.24nn  44157  jm2.17b  44159  jm2.17c  44160  jm2.24  44161  congadd  44164  congsym  44166  congneg  44167  congid  44169  mzpcong  44170  acongrep  44178  acongeq  44181  jm2.18  44186  jm2.19  44191  jm2.23  44194  jm2.25  44197  jm2.26lem3  44199  jm2.15nn0  44201  jm2.16nn0  44202  jm2.27a  44203  jm2.27c  44205  jm3.1lem1  44215  idomsubgmo  44385  sqrtcval  44831  inductionexd  45345  imo72b2lem0  45355  imo72b2  45362  dvgrat  45486  radcnvrat  45488  binomcxplemnn0  45523  binomcxplemnotnn0  45530  cncmpmax  46252  rnmptlb  46458  zltlesub  46504  infxrpnf  46659  xrpnf  46698  fmul01  46795  fmul01lt1lem1  46799  climdivf  46827  sumnnodd  46845  climinf2lem  46919  limsup10exlem  46985  climliminf  47019  dfxlim2v  47060  xlimliminflimsup  47075  dvdivbd  47136  volge0  47174  stoweidlem1  47214  stoweidlem16  47229  stoweidlem18  47231  stoweidlem24  47237  stoweidlem26  47239  stoweidlem36  47249  stoweidlem38  47251  stoweidlem41  47254  stoweidlem42  47255  stoweidlem44  47257  stoweidlem45  47258  stoweidlem48  47261  stoweidlem62  47275  wallispilem5  47282  stirlinglem1  47287  stirlinglem5  47291  stirlinglem7  47293  stirlinglem8  47294  stirlinglem9  47295  stirlinglem11  47297  fourierdlem4  47324  fourierdlem10  47330  fourierdlem37  47357  fourierdlem47  47366  fourierdlem72  47391  fourierdlem74  47393  fourierdlem79  47398  fourierdlem82  47401  fourierdlem89  47408  fourierdlem91  47410  fourierdlem93  47412  fourierdlem103  47422  fourierdlem104  47423  fourierdlem112  47431  etransclem24  47471  etransclem25  47472  etransclem28  47475  etransclem37  47484  etransclem38  47485  etransclem44  47491  meaiuninc3v  47697  vonicclem1  47896  pimconstlt0  47914  smfsuplem1  48024  chnerlem1  48095  rlimdmafv  48450  rlimdmafv2  48531  2elfz2melfz  48591  2timesltsq  48651  muldvdsfacgt  48659  iccpartgtprec  48705  iccpartlt  48709  iccpartgtl  48711  sqrtpwpw2p  48826  fmtnodvds  48832  goldbachthlem1  48833  lighneallem4a  48896  nprmdvdsfacm1lem1  48908  perfectALTVlem1  49022  uhgrimgrlim  49288  cznnring  49562  altgsumbcALT  49668  expnegico01  49833  flnn0div2ge  49848  rege1logbrege0  49873  fllogbd  49875  nnpw2blen  49895  nnolog2flm1  49905  dignn0ldlem  49917  dignn0flhalflem1  49930  dignn0flhalflem2  49931  eenglngeehlnmlem2  50054  itsclc0yqsol  50079  2itscp  50096  itscnhlinecirc02plem1  50097  itscnhlinecirc02plem2  50098  inlinecirc02p  50102