Theorem eqbrtri 3356

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

Syntax hints:   = wceq 1298   class class class wbr 3338

This theorem is referenced by:  eqbrtrri 3358  3brtr4i 3365  aleph1 6019  pm110.643 6072  cda0en 6075  xp1en 6077  mapcdaen 6082  halflt1 7216  sqlecan 7887  sqrlem6 7928  sqrlem10 7932  sqrlem11 7933  sqrlem19 7941  nthruz 7996  faclbnd3 8199  cvgcmpubi 8446  geolim 8499  geolim1 8501  0.999... 8508  ivthlem5 8547  dsupivthlem 8553  efcltlem1 8566  erelem2 8582  ege2lem2 8590  ege2le3lem2 8591  efaddlem20 8619  reeff1olem1 8689  cos2bnd 8741  sin4lt0 8747  ruclem31 8809  ruclem32 8810  aleph1re 8820  infxpdom 8840  ipcl 9704  pilem1 10020  efifolem1 10076  norm3difi 10647  norm3adifii 10648  bcsiALT 10679  occllem1 10806  occllem5 10810  projlem3 10821  projlem5 10823  projlem7 10825  projlem18 10836  nmopsetn0 11429  nmfnsetn0 11442  nmopge0 11472  nmfnge0 11488  0bdop 11555  opsqrlem6 11716  1nprm 13769  2prm 13779  cntrsetlem 14999  ufilen 15579  fsumltisumi 15823  bfplem6 16003

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