Theorem breqtrri 4029

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

Syntax hints:   = wceq 1353   class class class wbr 4002

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4003

This theorem is referenced by:  3brtr4i  4032  ensn1  6793  pw1dom2  7223  0lt1sr  7761  0le2  9005  2pos  9006  3pos  9009  4pos  9012  5pos  9015  6pos  9016  7pos  9017  8pos  9018  9pos  9019  1lt2  9084  2lt3  9085  3lt4  9087  4lt5  9090  5lt6  9094  6lt7  9099  7lt8  9105  8lt9  9112  nn0le2xi  9222  numltc  9405  declti  9417  sqge0i  10601  faclbnd2  10715  ege2le3  11672  cos2bnd  11761  3dvdsdec  11862  n2dvdsm1  11910  n2dvds3  11912  pockthi  12348  dveflem  14058  tangtx  14130  lgsdir2lem2  14301  ex-fl  14337