Theorem breqtrr 2640

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 1479	. 2 |- B = C
4	1, 3	breqtr 2638	1 |- ARC

Syntax hints:   = wceq 956   class class class wbr 2619

This theorem is referenced by:  3brtr4 2643  ensn1 4424  uncdadom 4921  xpcdaen 4931  0lt1sr 5204  2pos 5989  3pos 5991  4pos 5992  5pos 5993  6pos 5994  7pos 5995  8pos 5996  9pos 5997  10pos 5998  1lt2 6028  nn0le2x 6134  sqge0 6628  nnlesq 6661  sqrlem8 6680  sqrlem9 6681  sqrlem10 6682  cjmulge0 6793  absge0 6840  faclbnd2 6946  isumsplit 7216  0.999... 7246  ivthlem5 7285  dsupivthlem 7291  efaddlem10 7347  efaddlem20 7357  efaddlem22 7359  ef1tllem 7381  ef01tllem1 7383  eirrlem5 7393  efgt0 7404  efm1legeo 7417  efcnlem2 7420  sin01bndlem1 7467  sin01bndlem2 7468  cos2bnd 7475  cos01gt0 7477  ruclem29 7538  ruclem35 7544  infxpidmlem12 7563  siilem2 8512  minveclem14 8558  pilem1 8671  pilem3 8673  sincos6thpi 8711  cosh111lem1 8714  efifolem1 8722  loge 8767  normlem6 8981  normlem7 8982  pjnorm 9666  unierr 10037

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620

Copyright terms: Public domain