Theorem eqbrtri 5137

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 5121	. 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)
4	1, 3	mpbir 234	1 ⊢ 𝐴𝑅𝐶

This proof depends on syntax axioms:   = wceq 1570   class class class wbr 5114

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

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 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115

This theorem is used by:  eqbrtrri  5139  3brtr4i  5146  0sdom1dom  9216  1sdom2dom  9224  infxpenc2  10025  dju1p1e2  10176  pwsdompw  10205  r1om  10245  aleph1  10574  canthp1lem1  10655  halflt1  12479  3halfnz  12693  declei  12770  numlti  12771  sqlecan  14265  discr  14296  faclbnd3  14348  hashunlei  14482  hashge2el2dif  14537  geo2lim  15955  0.999...  15961  geoihalfsum  15962  cos2bnd  16269  sin4lt0  16276  eirrlem  16285  rpnnen2lem3  16297  rpnnen2lem9  16303  aleph1re  16326  1nprm  16762  strle2  17244  strle3  17245  1strstr  17308  2strstr  17312  rngstr  17376  srngstr  17387  lmodstr  17403  ipsstr  17414  phlstr  17424  topgrpstr  17439  otpsstr  17454  odrngstr  17481  imasvalstr  17529  chnub  18703  0frgp  19880  cnfldstr  21561  iscmet3lem3  25486  mbfimaopnlem  25851  mbfsup  25860  mbfi1fseqlem6  25916  aalioulem3  26534  aaliou3lem3  26544  dvradcnv  26621  logi  26789  asin1  27096  log2cnv  27146  log2tlbnd  27147  mule1  27349  bposlem5  27489  bposlem8  27492  zabsle1  27497  trkgstr  28750  0pth  30513  ex-fl  30835  blocnilem  31193  norm3difi  31536  norm3adifii  31537  bcsiALT  31568  nmopsetn0  32254  nmfnsetn0  32267  nmopge0  32300  nmfnge0  32316  0bdop  32382  nmcexi  32415  opsqrlem6  32534  dp2lt10  33240  dplti  33261  dpmul4  33270  idlsrgstr  33823  locfinref  34262  dya2iocct  34702  signswch  34980  hgt750lem  35070  hgt750lem2  35071  subfaclim  35701  faclim  36259  cnndvlem1  37167  taupilem2  38007  cntotbnd  38488  60gcd7e1  42813  3lexlogpow5ineq1  42862  aks4d1p1p7  42882  acos1half  43160  diophren  43581  algstr  43941  pr2dom  44294  tr3dom  44295  binomcxplemnn0  45100  binomcxplemrat  45101  stirlinglem1  46829  dirkercncflem1  46858  fouriersw  46986  meaiunlelem  47223  nthrucw  47648  ceilhalf1  48116  nfermltl2rev  48549  evengpoap3  48605  exple2lt6  49185  nnlog2ge0lt1  49387  catbas  50045  cathomfval  50046  catcofval  50047