Theorem breqtrr 2630

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	eqcomi 1471	. 2 |- B = C
4	1, 3	breqtr 2628	1 |- ARC

Syntax hints:   = wceq 953   class class class wbr 2609

This theorem is referenced by:  3brtr4 2633  ensn1 4405  uncdadom 4893  xpcdaen 4903  0lt1sr 5176  2pos 5936  3pos 5938  4pos 5939  5pos 5940  6pos 5941  7pos 5942  8pos 5943  9pos 5944  10pos 5945  1lt2 5975  nn0le2x 6081  sqge0 6559  nnlesq 6591  sqrlem8 6610  sqrlem9 6611  sqrlem10 6612  cjmulge0 6728  absge0 6775  faclbnd2 6883  isumsplit 7151  0.999... 7181  ivthlem5 7220  dsupivthlem 7226  ivthlem5OLD 7229  efaddlem10 7289  efaddlem20 7299  efaddlem22 7301  ef1tllem 7323  ef01tllem1 7325  eirrlem5 7334  efgt0 7345  efm1legeo 7357  efcnlem2 7360  sin01bndlem1 7409  sin01bndlem2 7410  cos2bnd 7417  cos01gt0 7419  ruclem29 7481  ruclem35 7487  infxpidmlem12 7506  siilem2 8443  minveclem14 8489  pilem1 8590  pilem3 8592  sincos6thpi 8628  cosh111lem1 8629  efifolem1 8637  loge 8689  logeOLD 8708  normlem6 8902  normlem7 8903  pjnorm 9583  unierr 9950

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610

Copyright terms: Public domain