Theorem eqbrtri 5125

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

This proof depends on syntax axioms:   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103

This theorem is used by:  eqbrtrri  5127  3brtr4i  5134  0sdom1dom  9241  1sdom2dom  9249  infxpenc2  10105  dju1p1e2  10256  pwsdompw  10285  aleph1  10660  canthp1lem1  10741  hfomALT  10865  halflt1  12567  3halfnz  12782  declei  12859  numlti  12860  sqlecan  14357  discr  14388  faclbnd3  14440  hashunlei  14574  hashge2el2dif  14629  geo2lim  16050  0.999...  16056  geoihalfsum  16057  cos2bnd  16362  sin4lt0  16369  eirrlem  16378  rpnnen2lem3  16390  rpnnen2lem9  16396  aleph1re  16419  1nprm  16860  strle2  17343  strle3  17344  1strstr  17407  2strstr  17411  rngstr  17475  srngstr  17486  lmodstr  17502  ipsstr  17513  phlstr  17523  topgrpstr  17538  otpsstr  17553  odrngstr  17580  imasvalstr  17628  chnub  18802  0frgp  19999  cnfldstr  21686  iscmet3lem3  25617  mbfimaopnlem  25982  mbfsup  25991  mbfi1fseqlem6  26047  aalioulem3  26667  aaliou3lem3  26677  dvradcnv  26754  logi  26921  asin1  27228  log2cnv  27278  log2tlbnd  27279  mule1  27481  bposlem5  27621  bposlem8  27624  zabsle1  27629  trkgstr  28912  0pth  30722  ex-fl  31054  blocnilem  31412  norm3difi  31755  norm3adifii  31756  bcsiALT  31787  nmopsetn0  32473  nmfnsetn0  32486  nmopge0  32519  nmfnge0  32535  0bdop  32601  nmcexi  32634  opsqrlem6  32753  dp2lt10  33497  dplti  33518  dpmul4  33527  idlsrgstr  34081  locfinref  34520  dya2iocct  34959  signswch  35237  hgt750lem  35327  hgt750lem2  35328  subfaclim  36040  faclim  36604  cnndvlem1  37496  taupilem2  38337  cntotbnd  38824  60gcd7e1  43149  3lexlogpow5ineq1  43198  aks4d1p1p7  43218  acos1half  43503  diophren  43914  algstr  44269  pr2dom  44622  tr3dom  44623  binomcxplemnn0  45427  binomcxplemrat  45428  stirlinglem1  47178  dirkercncflem1  47207  fouriersw  47335  meaiunlelem  47572  numtowerdt  48010  ceilhalf1  48502  nfermltl2rev  48935  evengpoap3  48991  exple2lt6  49570  nnlog2ge0lt1  49772  catbas  50442  cathomfval  50443  catcofval  50444