Theorem breqtrd 2636

Description: Substitution of equal classes into a binary relation.

Hypotheses

Ref	Expression
breqtrd.1	|- (ph -> ARB)
breqtrd.2	|- (ph -> B = C)

Assertion

Ref	Expression
breqtrd	|- (ph -> ARC)

Proof of Theorem breqtrd

Step	Hyp	Ref	Expression
1		breqtrd.1	. 2 |- (ph -> ARB)
2		breqtrd.2	. . 3 |- (ph -> B = C)
3	2	breq2d 2627	. 2 |- (ph -> (ARB <-> ARC))
4	1, 3	mpbid 195	1 |- (ph -> ARC)

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

This theorem is referenced by:  breqtrrd 2638  syl5breq 2647  phplem4 4504  ltm1t 5785  recp1lt1 5863  recrecltt 5864  ledivp1t 5867  ledivp1 5868  ltdivp1 5869  fladdzt 6204  exple1t 6557  expubndt 6558  bernneq 6602  discrlem3 6608  bcxmas 7044  climge0 7080  climaddc2 7088  climmullem5 7093  climsub 7099  clim2serzt 7103  clim2serz 7114  climcau 7125  georeclim 7211  cvgratlem2ALT 7219  cvgratlem2 7222  efcvgfsum 7293  erelem3 7299  reeff1 7386  sinbndt 7443  cosbndt 7444  sin01bndlem3 7447  cos01bndlem3 7449  sin01gt0 7454  cos01gt0 7455  sin02gt0 7456  infmap2 7560  metsym 7795  cnmet 7887  bcthlem24 8005  nvge0 8287  nmoub3i 8421  nmoub2i 8422  nmlno0lem 8438  minveclem19 8547  minveclem38 8566  htthlem6 8608  sinq12gt0t 8689  norm3dif2t 9002  bcs2t 9037  pjthlem10 9216  eigpos 9753  nmopub2tALT 9824  nmfnleub2t 9841  nmlnop0ALT 9911  riesz1t 9989  cnlnadjlem2 9992  nmopcoadj 10025  leopsqt 10053  leopmult 10058  leopnmidt 10062  nmopleidt 10063  hstle1t 10144  strlem3a 10170  mdslmd4 10251  cvexchlem 10286  cdj1 10351  msra3 10582

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 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1810  df-un 2048  df-sn 2410  df-pr 2411  df-op 2414  df-br 2617

Copyright terms: Public domain