Theorem eqbrtrr 2636

Description: Substitution of equal classes into a binary relation.

Hypotheses

Ref	Expression
eqbrtrr.1	|- A = B
eqbrtrr.2	|- ARC

Assertion

Ref	Expression
eqbrtrr	|- BRC

Proof of Theorem eqbrtrr

Step	Hyp	Ref	Expression
1		eqbrtrr.1	. . 3 |- A = B
2	1	eqcomi 1479	. 2 |- B = A
3		eqbrtrr.2	. 2 |- ARC
4	2, 3	eqbrtr 2634	1 |- BRC

Syntax hints:   = wceq 956   class class class wbr 2619

This theorem is referenced by:  3brtr3 2642  nnlesq 6661  nnesq 6662  sqrlem1 6673  sqrlem11 6683  sqrlem15 6687  sqr2gt1lt2 6719  sqr2irrlem1 6724  faclbnd4lem1 6948  bcpasc 6969  geolim1i 7238  erelem6 7324  efcj 7336  efaddlem22 7359  eftlexOLD 7377  effsumle 7397  efm1lim 7411  eflegeolem2 7414  efm1legeo 7417  reeff1olem1 7424  cos1bnd 7474  cos2bnd 7475  infdif 7568  sincos6thpi 8711  cosh111lem1 8714  efifolem3 8724  efifolem4 8725  efifolem6 8727  norm-ii 9004  projlem13 9198  projlem15 9200  nmopadj 10023  unierr 10037  boe 10460

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