Theorem eqbrtrri 4473

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
eqbrtrr.1
eqbrtrr.2

Assertion

Ref	Expression
eqbrtrri

Proof of Theorem eqbrtrri

Step	Hyp	Ref	Expression
1		eqbrtrr.1	. . 3
2	1	eqcomi 2470	. 2
3		eqbrtrr.2	. 2
4	2, 3	eqbrtri 4471	1

Syntax hints:  =wceq 1395   class class class wbr 4452

This theorem is referenced by:  3brtr3i  4479  expnass  12273  faclbnd4lem1  12371  sqrt2gt1lt2  13108  cos1bnd  13922  cos2bnd  13923  prdsvalstr  14850  ovolre  21936  pige3  22910  atan1  23259  log2ublem1  23277  sqrtlim  23302  bposlem8  23566  chebbnd1  23657  konigsberg  24987  norm-ii-i  26054  nmopadji  27009  unierri  27023  ballotlem2  28427  stoweidlem26  31808  wallispilem5  31851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453