Theorem breqtrri 3362

Description: Substitution of equal classes into a binary relation.

Hypotheses

Ref	Expression
breqtrr.1	|- ARB
breqtrr.2	|- C = B

Assertion

Ref	Expression
breqtrri	|- ARC

Proof of Theorem breqtrri

Step	Hyp	Ref	Expression
1		breqtrr.1	. 2 |- ARB
2		breqtrr.2	. . 3 |- C = B
3	2	eqcomi 1888	. 2 |- B = C
4	1, 3	breqtri 3360	1 |- ARC

Syntax hints:   = wceq 1298   class class class wbr 3338

This theorem is referenced by:  3brtr4i 3365  ensn1 5483  uncdadom 6069  xpcdaen 6081  0lt1sr 6356  2pos 7173  3pos 7175  4pos 7176  5pos 7177  6pos 7178  7pos 7179  8pos 7180  9pos 7181  10pos 7182  1lt2 7212  2lt3 7213  nn0le2xi 7343  sqge0i 7873  nnlesqi 7911  sqrlem8 7930  sqrlem9 7931  sqrlem10 7932  cjmulge0i 8043  absge0i 8091  faclbnd2 8198  isumspliti 8477  0.999... 8508  ivthlem5 8547  dsupivthlem 8553  efaddlem10 8609  efaddlem20 8619  efaddlem22 8621  ef1tllem 8643  ef01tllem1 8645  eirrlem5 8655  efgt0i 8669  efm1legeoi 8682  efcnlem2 8685  sin01bndlem1 8733  sin01bndlem2 8734  cos2bnd 8741  cos01gt0 8743  ruclem29 8807  ruclem35 8813  infxpidmlem12 8832  siilem2 9853  minveclem14 9903  pilem1 10020  pilem3 10022  sincos6thpi 10061  cosh111lem1 10068  efifolem1 10076  loge 10121  normlem6 10614  normlem7 10615  cm2mi 11202  pjnormi 11301  unierri 11674  divalglem2 13698  absrdbnd 15799  fdc 15812  fsumltisumii 15822  fsumleisumii 15825  heiborlem32 15986  bfplem4 16001  bfp 16009  pcoass 16085

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-un 2600  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339

Copyright terms: Public domain