Theorem eqbrtrrd 2633

Description: Substitution of equal classes into a binary relation.

Hypotheses

Ref	Expression
eqbrtrrd.1	|- (ph -> A = B)
eqbrtrrd.2	|- (ph -> ARC)

Assertion

Ref	Expression
eqbrtrrd	|- (ph -> BRC)

Proof of Theorem eqbrtrrd

Step	Hyp	Ref	Expression
1		eqbrtrrd.1	. . 3 |- (ph -> A = B)
2	1	eqcomd 1478	. 2 |- (ph -> B = A)
3		eqbrtrrd.2	. 2 |- (ph -> ARC)
4	2, 3	eqbrtrd 2631	1 |- (ph -> BRC)

Syntax hints:   -> wi 3   = wceq 955   class class class wbr 2615

This theorem is referenced by:  fodomfi 4549  lemulge11t 5814  flhalft 6201  ser1mono 6287  abs3dift 6851  abs2dift 6854  caubnd 6878  facwordit 6896  faclbnd4lem1 6900  facavgt 6907  fsumcmp0 6994  fsumabs 6996  serzcmp0 7008  2climnn 7055  2climnn0 7056  climmullem3 7075  climre 7104  climim 7105  climcau 7109  caucvg 7116  ser1cmp0 7128  isumclim5t 7154  recncf 7228  imcncf 7229  efcnlem1 7376  sin01bndlem3 7428  cos01bndlem3 7430  unctb 7537  bcthlem26 7986  nvabs 8265  normpyct 8968  nmophm 9917  lnopcon 9919  lnfncon 9946  hmopidmchlem 10034  hstlet 10113  hstlest 10114  stle 10123  mslb1 10545

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-un 2047  df-sn 2409  df-pr 2410  df-op 2413  df-br 2616

Copyright terms: Public domain