Theorem breqtr 2634

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 2623	. 2 |- (ARB <-> ARC)
4	1, 3	mpbi 189	1 |- ARC

Syntax hints:   = wceq 955   class class class wbr 2615

This theorem is referenced by:  breqtrr 2636  3brtr3 2638  cdacomen 4912  cdaassen 4913  lt01 5663  sqrlem10 6627  sqrlem11 6628  sqr2gt1lt2 6664  abslt 6825  absle 6826  absltOLD 6827  absleOLD 6828  abstri 6844  infcvglem2 7174  expcnvlem2 7180  geolimilem 7187  erelem2 7279  efaddlem16 7312  ef1tllem 7340  eirrlem3 7349  cos1bnd 7433  cos2bnd 7434  cos01gt0 7436  sin4lt0 7440  ruclem30 7499  siilem1 8470  sincos4thpi 8662  cosh111lem1 8664  normlem5 8935  normlem6 8936  norm-ii 8959  norm3adif 8970  projlem3 9143  projlem18 9158  cmm2 9507  nmopcoadj 9990  mdoc2 10309  dmdoc2 10311

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-un 2047  df-sn 2409  df-pr 2410  df-op 2413  df-br 2616

Copyright terms: Public domain