Theorem breqtr 2638

Description: Substitution of equal classes into a binary relation.

Hypotheses

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

Assertion

Ref	Expression
breqtr	|- ARC

Proof of Theorem breqtr

Step	Hyp	Ref	Expression
1		breqtr.1	. 2 |- ARB
2		breqtr.2	. . 3 |- B = C
3	2	breq2i 2627	. 2 |- (ARB <-> ARC)
4	1, 3	mpbi 189	1 |- ARC

Syntax hints:   = wceq 956   class class class wbr 2619

This theorem is referenced by:  breqtrr 2640  3brtr3 2642  cdacomen 4929  cdaassen 4930  lt01 5680  sqrlem10 6682  sqrlem11 6683  sqr2gt1lt2 6719  abslt 6875  absle 6876  abstri 6891  infcvglem2 7222  expcnvlem2 7228  geolimilem 7235  erelem2 7320  efaddlem16 7353  ef1tllem 7381  eirrlem3 7391  cos1bnd 7474  cos2bnd 7475  cos01gt0 7477  sin4lt0 7481  ruclem30 7539  siilem1 8511  sincos4thpi 8710  cosh111lem1 8714  normlem5 8980  normlem6 8981  norm-ii 9004  norm3adif 9015  projlem3 9188  projlem18 9203  cmm2 9550  nmopcoadj 10034  mdoc2 10353  dmdoc2 10355

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