Theorem eqbrtr 2629

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

Syntax hints:   = wceq 954   class class class wbr 2614

This theorem is referenced by:  eqbrtrr 2631  3brtr4 2638  unifi 4538  pwfi 4551  aleph1 4851  pm110.643 4903  cda0en 4905  xp1en 4907  mapcdaen 4912  halflt1 5985  sqlecant 6580  sqrlem6 6616  sqrlem10 6620  sqrlem11 6621  sqrlem19 6629  nthruz 6685  faclbnd3 6892  cvgcmpub 7129  geolim 7180  geolim1 7182  0.999... 7189  ivthlem5 7228  dsupivthlem 7234  ivthlem5OLD 7237  efcltlem1 7254  erelem2 7270  ege2lem2 7278  ege2le3lem2 7279  efaddlem20 7307  reeff1olem1 7372  reeff1olem1OLD 7374  cos2bnd 7425  sin4lt0 7431  ruclem31 7491  ruclem32 7492  aleph1re 7502  infxpdom 7522  ipcl 8312  pilem1 8609  efifolem1 8656  norm3dif 8953  norm3adif 8954  bcsALT 8985  occllem1 9112  occllem5 9116  projlem3 9127  projlem5 9129  projlem7 9131  projlem18 9142  nmopsetn0 9732  nmfnsetn0 9745  nmopge0t 9774  nmfnge0t 9790  0bdop 9856

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409  df-op 2412  df-br 2615

Copyright terms: Public domain