Theorem eqbrtri 4604

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

Syntax hints:   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  eqbrtrri  4606  3brtr4i  4613  infxpenc2  8728  pm110.643  8882  pwsdompw  8909  r1om  8949  aleph1  9272  canthp1lem1  9353  pwxpndom2  9366  neg1lt0  11004  halflt1  11127  3halfnz  11332  declei  11418  numlti  11421  sqlecan  12833  discr  12863  faclbnd3  12941  hashunlei  13072  hashge2el2dif  13117  geo2lim  14445  0.999...  14451  0.999...OLD  14452  geoihalfsum  14453  cos2bnd  14757  sin4lt0  14764  eirrlem  14771  rpnnen2lem3  14784  rpnnen2lem9  14790  aleph1re  14813  1nprm  15230  strle2  15801  strle3  15802  1strstr  15805  2strstr  15809  rngstr  15823  srngfn  15831  lmodstr  15840  ipsstr  15847  phlstr  15857  topgrpstr  15865  otpsstr  15874  otpsstrOLD  15878  odrngstr  15889  imasvalstr  15935  0frgp  18015  cnfldstr  19569  zlmlem  19684  tnglem  22254  iscmet3lem3  22896  mbfimaopnlem  23228  mbfsup  23237  mbfi1fseqlem6  23293  aalioulem3  23893  aaliou3lem3  23903  dvradcnv  23979  asin1  24421  log2cnv  24471  log2tlbnd  24472  mule1  24674  bposlem5  24813  bposlem8  24816  zabsle1  24821  trkgstr  25143  0pth  26100  ex-fl  26696  blocnilem  27043  norm3difi  27388  norm3adifii  27389  bcsiALT  27420  nmopsetn0  28108  nmfnsetn0  28121  nmopge0  28154  nmfnge0  28170  0bdop  28236  nmcexi  28269  opsqrlem6  28388  locfinref  29236  dya2iocct  29669  signswch  29964  subfaclim  30424  logi  30873  faclim  30885  cnndvlem1  31698  taupilem2  32345  cntotbnd  32765  diophren  36395  algstr  36766  binomcxplemnn0  37570  binomcxplemrat  37571  stirlinglem1  38967  dirkercncflem1  38996  fouriersw  39124  meaiunlelem  39361  evengpoap3  40215  0pth-av  41293  exple2lt6  41939  nnlog2ge0lt1  42158