Theorem eqbrtri 4826

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

Syntax hints:   = wceq 1632   class class class wbr 4805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-br 4806

This theorem is referenced by:  eqbrtrri  4828  3brtr4i  4835  infxpenc2  9056  pm110.643  9212  pwsdompw  9239  r1om  9279  aleph1  9606  canthp1lem1  9687  pwxpndom2  9700  neg1lt0  11340  halflt1  11463  3halfnz  11669  declei  11755  numlti  11758  sqlecan  13186  discr  13216  faclbnd3  13294  hashunlei  13425  hashge2el2dif  13475  geo2lim  14826  0.999...  14832  0.999...OLD  14833  geoihalfsum  14834  cos2bnd  15138  sin4lt0  15145  eirrlem  15152  rpnnen2lem3  15165  rpnnen2lem9  15171  aleph1re  15194  1nprm  15615  strle2  16197  strle3  16198  1strstr  16202  2strstr  16206  rngstr  16223  srngfn  16231  lmodstr  16240  ipsstr  16247  phlstr  16257  topgrpstr  16265  otpsstr  16274  otpsstrOLD  16278  odrngstr  16289  imasvalstr  16335  0frgp  18413  cnfldstr  19971  zlmlem  20088  tnglem  22666  iscmet3lem3  23309  mbfimaopnlem  23642  mbfsup  23651  mbfi1fseqlem6  23707  aalioulem3  24309  aaliou3lem3  24319  dvradcnv  24395  asin1  24842  log2cnv  24892  log2tlbnd  24893  mule1  25095  bposlem5  25234  bposlem8  25237  zabsle1  25242  trkgstr  25564  0pth  27299  ex-fl  27637  blocnilem  27990  norm3difi  28335  norm3adifii  28336  bcsiALT  28367  nmopsetn0  29055  nmfnsetn0  29068  nmopge0  29101  nmfnge0  29117  0bdop  29183  nmcexi  29216  opsqrlem6  29335  dp2lt10  29922  dplti  29944  dpmul4  29953  locfinref  30239  dya2iocct  30673  signswch  30969  hgt750lem  31060  hgt750lem2  31061  subfaclim  31499  logi  31949  faclim  31961  cnndvlem1  32856  taupilem2  33498  cntotbnd  33927  diophren  37898  algstr  38268  binomcxplemnn0  39069  binomcxplemrat  39070  stirlinglem1  40813  dirkercncflem1  40842  fouriersw  40970  meaiunlelem  41207  evengpoap3  42216  exple2lt6  42674  nnlog2ge0lt1  42889