Theorem eqbrtr 2634

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

Syntax hints:   = wceq 956   class class class wbr 2619

This theorem is referenced by:  eqbrtrr 2636  3brtr4 2643  unifiOLD 4557  pwfiOLD 4571  aleph1 4871  pm110.643 4923  cda0en 4925  xp1en 4927  mapcdaen 4932  halflt1 6030  sqlecant 6641  sqrlem6 6678  sqrlem10 6682  sqrlem11 6683  sqrlem19 6691  nthruz 6746  faclbnd3 6947  cvgcmpub 7185  geolim 7237  geolim1 7239  0.999... 7246  ivthlem5 7285  dsupivthlem 7291  efcltlem1 7304  erelem2 7320  ege2lem2 7328  ege2le3lem2 7329  efaddlem20 7357  reeff1olem1 7424  cos2bnd 7475  sin4lt0 7481  ruclem31 7540  ruclem32 7541  aleph1re 7551  infxpdom 7571  ipcl 8365  pilem1 8671  efifolem1 8722  norm3dif 9014  norm3adif 9015  bcsALT 9046  occllem1 9173  occllem5 9177  projlem3 9188  projlem5 9190  projlem7 9192  projlem18 9203  nmopsetn0 9792  nmfnsetn0 9805  nmopge0t 9835  nmfnge0t 9851  0bdop 9918

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