Theorem eqbrtri 4983

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

Syntax hints:   = wceq 1522   class class class wbr 4962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-br 4963

This theorem is referenced by:  eqbrtrri  4985  3brtr4i  4992  infxpenc2  9294  dju1p1e2  9445  pwsdompw  9472  r1om  9512  aleph1  9839  canthp1lem1  9920  neg1lt0  11602  halflt1  11703  3halfnz  11910  declei  11983  numlti  11984  sqlecan  13421  discr  13451  faclbnd3  13502  hashunlei  13634  hashge2el2dif  13684  geo2lim  15064  0.999...  15070  geoihalfsum  15071  cos2bnd  15374  sin4lt0  15381  eirrlem  15390  rpnnen2lem3  15402  rpnnen2lem9  15408  aleph1re  15431  1nprm  15852  strle2  16422  strle3  16423  1strstr  16427  2strstr  16431  rngstr  16448  srngstr  16456  lmodstr  16465  ipsstr  16472  phlstr  16482  topgrpstr  16490  otpsstr  16497  odrngstr  16508  imasvalstr  16554  0frgp  18632  cnfldstr  20229  zlmlem  20346  tnglem  22932  iscmet3lem3  23576  mbfimaopnlem  23939  mbfsup  23948  mbfi1fseqlem6  24004  aalioulem3  24606  aaliou3lem3  24616  dvradcnv  24692  asin1  25153  log2cnv  25204  log2tlbnd  25205  mule1  25407  bposlem5  25546  bposlem8  25549  zabsle1  25554  trkgstr  25912  0pth  27591  ex-fl  27918  blocnilem  28272  norm3difi  28615  norm3adifii  28616  bcsiALT  28647  nmopsetn0  29333  nmfnsetn0  29346  nmopge0  29379  nmfnge0  29395  0bdop  29461  nmcexi  29494  opsqrlem6  29613  dp2lt10  30244  dplti  30265  dpmul4  30274  locfinref  30722  dya2iocct  31155  signswch  31448  hgt750lem  31539  hgt750lem2  31540  subfaclim  32043  logi  32574  faclim  32586  cnndvlem1  33485  taupilem2  34134  cntotbnd  34606  diophren  38895  algstr  39262  pr2dom  39378  tr3dom  39379  binomcxplemnn0  40219  binomcxplemrat  40220  stirlinglem1  41901  dirkercncflem1  41930  fouriersw  42058  meaiunlelem  42292  nfermltl2rev  43390  evengpoap3  43446  exple2lt6  43892  nnlog2ge0lt1  44107