Theorem eqbrtri 5087

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

Syntax hints:   = wceq 1537   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  eqbrtrri  5089  3brtr4i  5096  infxpenc2  9448  dju1p1e2  9599  pwsdompw  9626  r1om  9666  aleph1  9993  canthp1lem1  10074  neg1lt0  11755  halflt1  11856  3halfnz  12062  declei  12135  numlti  12136  sqlecan  13572  discr  13602  faclbnd3  13653  hashunlei  13787  hashge2el2dif  13839  geo2lim  15231  0.999...  15237  geoihalfsum  15238  cos2bnd  15541  sin4lt0  15548  eirrlem  15557  rpnnen2lem3  15569  rpnnen2lem9  15575  aleph1re  15598  1nprm  16023  strle2  16593  strle3  16594  1strstr  16598  2strstr  16602  rngstr  16619  srngstr  16627  lmodstr  16636  ipsstr  16643  phlstr  16653  topgrpstr  16661  otpsstr  16668  odrngstr  16679  imasvalstr  16725  0frgp  18905  cnfldstr  20547  zlmlem  20664  tnglem  23249  iscmet3lem3  23893  mbfimaopnlem  24256  mbfsup  24265  mbfi1fseqlem6  24321  aalioulem3  24923  aaliou3lem3  24933  dvradcnv  25009  asin1  25472  log2cnv  25522  log2tlbnd  25523  mule1  25725  bposlem5  25864  bposlem8  25867  zabsle1  25872  trkgstr  26230  0pth  27904  ex-fl  28226  blocnilem  28581  norm3difi  28924  norm3adifii  28925  bcsiALT  28956  nmopsetn0  29642  nmfnsetn0  29655  nmopge0  29688  nmfnge0  29704  0bdop  29770  nmcexi  29803  opsqrlem6  29922  dp2lt10  30560  dplti  30581  dpmul4  30590  locfinref  31105  dya2iocct  31538  signswch  31831  hgt750lem  31922  hgt750lem2  31923  subfaclim  32435  logi  32966  faclim  32978  cnndvlem1  33876  taupilem2  34606  cntotbnd  35089  diophren  39430  algstr  39797  pr2dom  39913  tr3dom  39914  binomcxplemnn0  40701  binomcxplemrat  40702  stirlinglem1  42379  dirkercncflem1  42408  fouriersw  42536  meaiunlelem  42770  nfermltl2rev  43928  evengpoap3  43984  exple2lt6  44432  nnlog2ge0lt1  44646