Theorem breqtri 3360

Description: Substitution of equal classes into a binary relation.

Hypotheses

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

Assertion

Ref	Expression
breqtri	|- ARC

Proof of Theorem breqtri

Step	Hyp	Ref	Expression
1		breqtr.1	. 2 |- ARB
2		breqtr.2	. . 3 |- B = C
3	2	breq2i 3346	. 2 |- (ARB <-> ARC)
4	1, 3	mpbi 206	1 |- ARC

Syntax hints:   = wceq 1298   class class class wbr 3338

This theorem is referenced by:  breqtrri 3362  3brtr3i 3364  cdacomen 6079  cdaassen 6080  lt01 6871  sqrlem10 7932  sqrlem11 7933  sqr2gt1lt2 7969  abslti 8127  abslei 8128  abstrii 8143  infcvglem2 8483  expcnvlem2 8489  geolimilem 8497  erelem2 8582  efaddlem16 8615  ef1tllem 8643  eirrlem3 8653  cos1bnd 8740  cos2bnd 8741  cos01gt0 8743  sin4lt0 8747  ruclem30 8808  siilem1 9852  sincos4thpi 10060  cosh111lem1 10068  normlem5 10613  normlem6 10614  norm-ii.i 10637  norm3adifii 10648  projlem3 10821  projlem18 10836  cmm2i 11183  mayetes3i 11310  nmopcoadji 11671  mdoc2i 11998  dmdoc2i 12000  gcdaddmlem 13734  4nprm 13781  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