Theorem eqbrtr 2602

Description: Substitution of equal classes into a binary relation.

Hypotheses

Ref	Expression
eqbrtr.1	|- A = B
eqbrtr.2	|- BRC

Assertion

Ref	Expression
eqbrtr	|- ARC

Proof of Theorem eqbrtr

Step	Hyp	Ref	Expression
1		eqbrtr.2	. 2 |- BRC
2		eqbrtr.1	. . 3 |- A = B
3	2	breq1i 2594	. 2 |- (ARC <-> BRC)
4	1, 3	mpbir 190	1 |- ARC

Syntax hints:   = wceq 1099   class class class wbr 2587

This theorem is referenced by:  eqbrtrr 2604  3brtr4 2611  unifi 4484  pwfi 4497  aleph1 4794  pm110.643 4846  cda0en 4848  xp1en 4850  mapcdaen 4855  halflt1 5928  sqlecant 6523  sqrlem6 6559  sqrlem10 6563  sqrlem11 6564  sqrlem19 6572  nthruz 6628  faclbnd3 6835  cvgcmpub 7072  geolim 7123  geolim1 7125  0.999... 7132  ivthlem5 7171  dsupivthlem 7177  ivthlem5OLD 7180  efcltlem1 7197  erelem2 7213  ege2lem2 7221  ege2le3lem2 7222  efaddlem20 7250  reeff1olem1 7315  reeff1olem1OLD 7317  cos2bnd 7368  sin4lt0 7374  ruclem31 7434  ruclem32 7435  aleph1re 7445  infxpdom 7465  ipcl 8234  pilem1 8503  efifolem1 8550  norm3dif 9163  norm3adif 9164  bcsALT 9195  occllem1 9303  occllem5 9307  projlem3 9318  projlem5 9320  projlem7 9322  projlem18 9333  nmopsetn0 9923  nmfnsetn0 9936  nmopge0t 9965  nmfnge0t 9981  0bdop 10047

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787  df-un 2021  df-sn 2383  df-pr 2384  df-op 2387  df-br 2588

Copyright terms: Public domain