Theorem breqtrri 4113

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

Syntax hints:   = wceq 1395   class class class wbr 4086

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  3brtr4i  4116  ensn1  6965  pw1dom2  7435  0lt1sr  7975  0le2  9223  2pos  9224  3pos  9227  4pos  9230  5pos  9233  6pos  9234  7pos  9235  8pos  9236  9pos  9237  1lt2  9303  2lt3  9304  3lt4  9306  4lt5  9309  5lt6  9313  6lt7  9318  7lt8  9324  8lt9  9331  nn0le2xi  9442  numltc  9626  declti  9638  sqge0i  10878  faclbnd2  10994  ege2le3  12222  cos2bnd  12311  3dvdsdec  12416  n2dvdsm1  12464  n2dvds3  12466  pockthi  12921  dec2dvds  12974  dveflem  15440  tangtx  15552  lgsdir2lem2  15748  ex-fl  16257