Theorem breqtrri 5116

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 2745	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtri 5114	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1540   class class class wbr 5089

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-sn 4573  df-pr 4575  df-op 4579  df-br 5090

This theorem is referenced by:  3brtr4i  5119  ensn1  8874  ensn1OLD  8875  1sdom2ALT  9098  dju1p1e2ALT  10023  infmap2  10067  0lt1sr  10944  0le2  12168  2pos  12169  3pos  12171  4pos  12173  5pos  12175  6pos  12176  7pos  12177  8pos  12178  9pos  12179  1lt2  12237  2lt3  12238  3lt4  12240  4lt5  12243  5lt6  12247  6lt7  12252  7lt8  12258  8lt9  12265  nn0le2xi  12380  numltc  12556  declti  12568  xlemul1a  13115  sqge0i  13998  faclbnd2  14098  cats1fv  14663  ege2le3  15890  cos2bnd  15988  3dvdsdec  16132  n2dvdsm1  16169  sumeven  16187  divalglem2  16195  pockthi  16697  dec2dvds  16853  prmlem1  16898  prmlem2  16910  1259prm  16926  2503prm  16930  4001prm  16935  2strstr1OLD  17027  vitalilem5  24874  dveflem  25241  tangtx  25760  sinq12ge0  25763  cxpge0  25936  asin1  26142  birthday  26202  lgamgulmlem4  26279  ppiub  26450  bposlem7  26536  lgsdir2lem2  26572  pthdlem2  28365  ex-fl  29040  ex-ind-dvds  29054  siilem2  29443  normlem6  29706  normlem7  29707  cm2mi  30217  pjnormi  30312  unierri  30695  dp2lt10  31386  dpgti  31408  pfx1s2  31441  cyc2fv2  31617  cyc3fv3  31634  hgt750lemd  32869  hgt750lem  32872  hgt750lem2  32873  hgt750leme  32879  logi  33934  cnndvlem1  34808  taupi  35592  poimirlem25  35900  poimirlem26  35901  poimirlem27  35902  poimirlem28  35903  ftc1anclem5  35952  fdc  36001  lcmineqlem23  40306  3lexlogpow2ineq2  40314  pellfundgt1  40955  jm2.27dlem2  41083  stoweidlem13  43879  sqwvfoura  44094  sqwvfourb  44095  fourierswlem  44096  41prothprm  45411  tgblthelfgott  45607  tgoldbachlt  45608  nnlog2ge0lt1  46252  1aryenefmnd  46332  ackval42  46382  tworepnotupword  46861