Theorem breqtrri 3992

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

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

Syntax hints:   = wceq 1335   class class class wbr 3966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-sn 3566  df-pr 3567  df-op 3569  df-br 3967

This theorem is referenced by:  3brtr4i  3995  ensn1  6742  pw1dom2  7163  0lt1sr  7686  0le2  8924  2pos  8925  3pos  8928  4pos  8931  5pos  8934  6pos  8935  7pos  8936  8pos  8937  9pos  8938  1lt2  9003  2lt3  9004  3lt4  9006  4lt5  9009  5lt6  9013  6lt7  9018  7lt8  9024  8lt9  9031  nn0le2xi  9141  numltc  9321  declti  9333  sqge0i  10509  faclbnd2  10620  ege2le3  11572  cos2bnd  11661  3dvdsdec  11760  n2dvdsm1  11808  n2dvds3  11810  dveflem  13129  tangtx  13201  ex-fl  13343