Theorem breqtrri 4032

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 4030	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1353   class class class wbr 4005

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 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006

This theorem is referenced by:  3brtr4i  4035  ensn1  6798  pw1dom2  7228  0lt1sr  7766  0le2  9011  2pos  9012  3pos  9015  4pos  9018  5pos  9021  6pos  9022  7pos  9023  8pos  9024  9pos  9025  1lt2  9090  2lt3  9091  3lt4  9093  4lt5  9096  5lt6  9100  6lt7  9105  7lt8  9111  8lt9  9118  nn0le2xi  9228  numltc  9411  declti  9423  sqge0i  10609  faclbnd2  10724  ege2le3  11681  cos2bnd  11770  3dvdsdec  11872  n2dvdsm1  11920  n2dvds3  11922  pockthi  12358  dveflem  14226  tangtx  14298  lgsdir2lem2  14469  ex-fl  14516