Theorem breqtrr 2082

Description: Substitution of equal classes into a binary relation.

Hypotheses

Ref	Expression
breqtrr.1	|- ARB
breqtrr.2	|- C = B

Assertion

Ref	Expression
breqtrr	|- ARC

Proof of Theorem breqtrr

Step	Hyp	Ref	Expression
1		breqtrr.1	. 2 |- ARB
2		breqtrr.2	. . 3 |- C = B
3	2	cleqcomi 1105	. 2 |- B = C
4	1, 3	breqtr 2080	1 |- ARC

Syntax hints:   = wceq 1091   class class class wbr 2054

This theorem is referenced by:  3brtr4 2085  ensn1 3329  uncdadom 3718  xpcdaen 3726  0lt1sr 3998  2pos 4479  3pos 4480  4pos 4481  5pos 4482  6pos 4483  7pos 4484  8pos 4485  9pos 4486  nn0le2x 4562  sqege0 4704  nnlesq 4718  nneo 4719  sqrlem8 4738  sqrlem9 4739  sqrlem10 4740  sqr2irrlem1 4777  cjmulge0 4823  absge0 4841  ruclem25 4909  ruclem29 4913  ruclem35 4919  infxpidmlem12 4944  normlem6 5068  normlem7 5069  pjnorm 5663

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-un 1490  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063

metamath.org