Theorem eqbrtri 5106

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

Hypotheses

Ref	Expression
eqbrtr.1	⊢ 𝐴 = 𝐵
eqbrtr.2	⊢ 𝐵𝑅𝐶

Assertion

Ref	Expression
eqbrtri	⊢ 𝐴𝑅𝐶

Proof of Theorem eqbrtri

Step	Hyp	Ref	Expression
1		eqbrtr.2	. 2 ⊢ 𝐵𝑅𝐶
2		eqbrtr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	breq1i 5092	. 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)
4	1, 3	mpbir 231	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1542   class class class wbr 5085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  eqbrtrri  5108  3brtr4i  5115  0sdom1dom  9156  1sdom2dom  9164  infxpenc2  9944  dju1p1e2  10096  pwsdompw  10125  r1om  10165  aleph1  10494  canthp1lem1  10575  halflt1  12394  3halfnz  12608  declei  12680  numlti  12681  sqlecan  14171  discr  14202  faclbnd3  14254  hashunlei  14387  hashge2el2dif  14442  geo2lim  15840  0.999...  15846  geoihalfsum  15847  cos2bnd  16155  sin4lt0  16162  eirrlem  16171  rpnnen2lem3  16183  rpnnen2lem9  16189  aleph1re  16212  1nprm  16648  strle2  17129  strle3  17130  1strstr  17193  2strstr  17197  rngstr  17261  srngstr  17272  lmodstr  17288  ipsstr  17299  phlstr  17309  topgrpstr  17324  otpsstr  17339  odrngstr  17366  imasvalstr  17414  chnub  18588  0frgp  19754  cnfldstr  21354  iscmet3lem3  25257  mbfimaopnlem  25622  mbfsup  25631  mbfi1fseqlem6  25687  aalioulem3  26300  aaliou3lem3  26310  dvradcnv  26386  logi  26551  asin1  26858  log2cnv  26908  log2tlbnd  26909  mule1  27111  bposlem5  27251  bposlem8  27254  zabsle1  27259  trkgstr  28512  0pth  30195  ex-fl  30517  blocnilem  30875  norm3difi  31218  norm3adifii  31219  bcsiALT  31250  nmopsetn0  31936  nmfnsetn0  31949  nmopge0  31982  nmfnge0  31998  0bdop  32064  nmcexi  32097  opsqrlem6  32216  dp2lt10  32943  dplti  32964  dpmul4  32973  idlsrgstr  33562  locfinref  33985  dya2iocct  34424  signswch  34705  hgt750lem  34795  hgt750lem2  34796  subfaclim  35370  faclim  35928  cnndvlem1  36797  taupilem2  37636  cntotbnd  38117  60gcd7e1  42444  3lexlogpow5ineq1  42493  aks4d1p1p7  42513  acos1half  42790  diophren  43241  algstr  43601  pr2dom  43954  tr3dom  43955  binomcxplemnn0  44776  binomcxplemrat  44777  stirlinglem1  46502  dirkercncflem1  46531  fouriersw  46659  meaiunlelem  46896  nthrucw  47316  ceilhalf1  47786  nfermltl2rev  48219  evengpoap3  48275  exple2lt6  48840  nnlog2ge0lt1  49042  catbas  49701  cathomfval  49702  catcofval  49703