Theorem eqbrtri 5163

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

Syntax hints:   = wceq 1534   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143

This theorem is referenced by:  eqbrtrri  5165  3brtr4i  5172  0sdom1dom  9254  1sdom2dom  9263  infxpenc2  10037  dju1p1e2  10188  pwsdompw  10219  r1om  10259  aleph1  10586  canthp1lem1  10667  neg1lt0  12351  halflt1  12452  3halfnz  12663  declei  12735  numlti  12736  sqlecan  14196  discr  14226  faclbnd3  14275  hashunlei  14408  hashge2el2dif  14465  geo2lim  15845  0.999...  15851  geoihalfsum  15852  cos2bnd  16156  sin4lt0  16163  eirrlem  16172  rpnnen2lem3  16184  rpnnen2lem9  16190  aleph1re  16213  1nprm  16641  strle2  17119  strle3  17120  1strstr  17186  1strstr1  17187  2strstr  17193  2strstr1  17196  rngstr  17270  srngstr  17281  lmodstr  17297  ipsstr  17308  phlstr  17318  topgrpstr  17333  otpsstr  17348  odrngstr  17375  imasvalstr  17424  0frgp  19725  cnfldstr  21268  cnfldstrOLD  21283  zlmlemOLD  21430  tnglemOLD  24537  iscmet3lem3  25205  mbfimaopnlem  25571  mbfsup  25580  mbfi1fseqlem6  25637  aalioulem3  26256  aaliou3lem3  26266  dvradcnv  26344  logi  26508  asin1  26813  log2cnv  26863  log2tlbnd  26864  mule1  27067  bposlem5  27208  bposlem8  27211  zabsle1  27216  trkgstr  28235  0pth  29922  ex-fl  30244  blocnilem  30601  norm3difi  30944  norm3adifii  30945  bcsiALT  30976  nmopsetn0  31662  nmfnsetn0  31675  nmopge0  31708  nmfnge0  31724  0bdop  31790  nmcexi  31823  opsqrlem6  31942  dp2lt10  32589  dplti  32610  dpmul4  32619  idlsrgstr  33149  locfinref  33378  dya2iocct  33836  signswch  34129  hgt750lem  34219  hgt750lem2  34220  subfaclim  34734  faclim  35276  cnndvlem1  35948  taupilem2  36737  cntotbnd  37204  60gcd7e1  41413  3lexlogpow5ineq1  41462  aks4d1p1p7  41482  acos1half  42019  diophren  42155  algstr  42523  pr2dom  42880  tr3dom  42881  binomcxplemnn0  43709  binomcxplemrat  43710  stirlinglem1  45385  dirkercncflem1  45414  fouriersw  45542  meaiunlelem  45779  nfermltl2rev  47006  evengpoap3  47062  exple2lt6  47351  nnlog2ge0lt1  47562