Theorem breqtrri 5093

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
breqtrr.1	⊢ 𝐴𝑅𝐵
breqtrr.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
breqtrri	⊢ 𝐴𝑅𝐶

Proof of Theorem breqtrri

Step	Hyp	Ref	Expression
1		breqtrr.1	. 2 ⊢ 𝐴𝑅𝐵
2		breqtrr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2830	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtri 5091	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:  3brtr4i  5096  ensn1  8573  1sdom2  8717  dju1p1e2ALT  9600  infmap2  9640  0lt1sr  10517  0le2  11740  2pos  11741  3pos  11743  4pos  11745  5pos  11747  6pos  11748  7pos  11749  8pos  11750  9pos  11751  1lt2  11809  2lt3  11810  3lt4  11812  4lt5  11815  5lt6  11819  6lt7  11824  7lt8  11830  8lt9  11837  nn0le2xi  11952  numltc  12125  declti  12137  xlemul1a  12682  sqge0i  13552  faclbnd2  13652  cats1fv  14221  ege2le3  15443  cos2bnd  15541  3dvdsdec  15681  n2dvdsm1  15719  n2dvds3OLD  15722  sumeven  15738  divalglem2  15746  pockthi  16243  dec2dvds  16399  prmlem1  16441  prmlem2  16453  1259prm  16469  2503prm  16473  4001prm  16478  2strstr1  16605  vitalilem5  24213  dveflem  24576  tangtx  25091  sinq12ge0  25094  cxpge0  25266  asin1  25472  birthday  25532  lgamgulmlem4  25609  ppiub  25780  bposlem7  25866  lgsdir2lem2  25902  pthdlem2  27549  ex-fl  28226  ex-ind-dvds  28240  siilem2  28629  normlem6  28892  normlem7  28893  cm2mi  29403  pjnormi  29498  unierri  29881  dp2lt10  30560  dpgti  30582  pfx1s2  30615  cyc2fv2  30764  cyc3fv3  30781  hgt750lemd  31919  hgt750lem  31922  hgt750lem2  31923  hgt750leme  31929  logi  32966  cnndvlem1  33876  taupi  34607  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  ftc1anclem5  34986  fdc  35035  pellfundgt1  39500  jm2.27dlem2  39627  stoweidlem13  42318  sqwvfoura  42533  sqwvfourb  42534  fourierswlem  42535  41prothprm  43804  tgblthelfgott  44000  tgoldbachlt  44001  nnlog2ge0lt1  44646