Theorem eqbrtri 2707

Description: Substitution of equal classes into a binary relation.

Hypotheses

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

Assertion

Ref	Expression
eqbrtri	|- ARC

Proof of Theorem eqbrtri

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

Syntax hints:   = wceq 992   class class class wbr 2692

This theorem is referenced by:  eqbrtrri 2709  3brtr4i 2716  aleph1 5021  pm110.643 5074  cda0en 5077  xp1en 5079  mapcdaen 5084  halflt1 6176  sqlecan 6838  sqrlem6 6879  sqrlem10 6883  sqrlem11 6884  sqrlem19 6892  nthruz 6947  faclbnd3 7150  cvgcmpubi 7389  geolim 7442  geolim1 7444  0.999... 7451  ivthlem5 7490  dsupivthlem 7496  efcltlem1 7509  erelem2 7525  ege2lem2 7533  ege2le3lem2 7534  efaddlem20 7562  reeff1olem1 7632  cos2bnd 7684  sin4lt0 7690  ruclem31 7752  ruclem32 7753  aleph1re 7763  infxpdom 7783  ipcl 8619  pilem1 8938  efifolem1 8994  norm3difi 9290  norm3adifii 9291  bcsiALT 9322  occllem1 9449  occllem5 9453  projlem3 9464  projlem5 9466  projlem7 9468  projlem18 9479  nmopsetn0 10072  nmfnsetn0 10085  nmopge0 10115  nmfnge0 10131  0bdop 10197  ufilen 11664  fsumltisumi 11886  bfplem6 12059

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102  df-sn 2470  df-pr 2471  df-op 2474  df-br 2693

Copyright terms: Public domain