Theorem breqtrri 4025

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

Hypotheses

Ref	Expression
breqtrr.1	|- A R B
breqtrr.2	|- C = B

Assertion

Ref	Expression
breqtrri	|- A R C

Proof of Theorem breqtrri

Step	Hyp	Ref	Expression
1		breqtrr.1	. 2 |- A R B
2		breqtrr.2	. . 3 |- C = B
3	2	eqcomi 2179	. 2 |- B = C
4	1, 3	breqtri 4023	1 |- A R C

Syntax hints:   = wceq 1353   class class class wbr 3998

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999

This theorem is referenced by:  3brtr4i  4028  ensn1  6786  pw1dom2  7216  0lt1sr  7739  0le2  8982  2pos  8983  3pos  8986  4pos  8989  5pos  8992  6pos  8993  7pos  8994  8pos  8995  9pos  8996  1lt2  9061  2lt3  9062  3lt4  9064  4lt5  9067  5lt6  9071  6lt7  9076  7lt8  9082  8lt9  9089  nn0le2xi  9199  numltc  9382  declti  9394  sqge0i  10576  faclbnd2  10690  ege2le3  11647  cos2bnd  11736  3dvdsdec  11837  n2dvdsm1  11885  n2dvds3  11887  pockthi  12323  dveflem  13758  tangtx  13830  lgsdir2lem2  14001  ex-fl  14037