Theorem eqbrtr 2624

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 2616	. 2 |- (ARC <-> BRC)
4	1, 3	mpbir 190	1 |- ARC

Syntax hints:   = wceq 953   class class class wbr 2609

This theorem is referenced by:  eqbrtrr 2626  3brtr4 2633  unifi 4532  pwfi 4545  aleph1 4843  pm110.643 4895  cda0en 4897  xp1en 4899  mapcdaen 4904  halflt1 5977  sqlecant 6572  sqrlem6 6608  sqrlem10 6612  sqrlem11 6613  sqrlem19 6621  nthruz 6677  faclbnd3 6884  cvgcmpub 7121  geolim 7172  geolim1 7174  0.999... 7181  ivthlem5 7220  dsupivthlem 7226  ivthlem5OLD 7229  efcltlem1 7246  erelem2 7262  ege2lem2 7270  ege2le3lem2 7271  efaddlem20 7299  reeff1olem1 7364  reeff1olem1OLD 7366  cos2bnd 7417  sin4lt0 7423  ruclem31 7483  ruclem32 7484  aleph1re 7494  infxpdom 7514  ipcl 8299  pilem1 8590  efifolem1 8637  norm3dif 8935  norm3adif 8936  bcsALT 8967  occllem1 9089  occllem5 9093  projlem3 9104  projlem5 9106  projlem7 9108  projlem18 9119  nmopsetn0 9709  nmfnsetn0 9722  nmopge0t 9751  nmfnge0t 9767  0bdop 9833

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610

Copyright terms: Public domain