Theorem breqtrri 4061

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 2200	. 2 |- B = C
4	1, 3	breqtri 4059	1 |- A R C

Syntax hints:   = wceq 1364   class class class wbr 4034

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  3brtr4i  4064  ensn1  6864  pw1dom2  7312  0lt1sr  7851  0le2  9099  2pos  9100  3pos  9103  4pos  9106  5pos  9109  6pos  9110  7pos  9111  8pos  9112  9pos  9113  1lt2  9179  2lt3  9180  3lt4  9182  4lt5  9185  5lt6  9189  6lt7  9194  7lt8  9200  8lt9  9207  nn0le2xi  9318  numltc  9501  declti  9513  sqge0i  10737  faclbnd2  10853  ege2le3  11855  cos2bnd  11944  3dvdsdec  12049  n2dvdsm1  12097  n2dvds3  12099  pockthi  12554  dec2dvds  12607  dveflem  15070  tangtx  15182  lgsdir2lem2  15378  ex-fl  15479