Theorem breqtrri 4057

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

Syntax hints:   = wceq 1364   class class class wbr 4030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031

This theorem is referenced by:  3brtr4i  4060  ensn1  6852  pw1dom2  7289  0lt1sr  7827  0le2  9074  2pos  9075  3pos  9078  4pos  9081  5pos  9084  6pos  9085  7pos  9086  8pos  9087  9pos  9088  1lt2  9154  2lt3  9155  3lt4  9157  4lt5  9160  5lt6  9164  6lt7  9169  7lt8  9175  8lt9  9182  nn0le2xi  9293  numltc  9476  declti  9488  sqge0i  10700  faclbnd2  10816  ege2le3  11817  cos2bnd  11906  3dvdsdec  12009  n2dvdsm1  12057  n2dvds3  12059  pockthi  12499  dveflem  14905  tangtx  15014  lgsdir2lem2  15186  ex-fl  15287