Theorem eqbrtrd 2631

Description: Substitution of equal classes into a binary relation.

Hypotheses

Ref	Expression
eqbrtrd.1	|- (ph -> A = B)
eqbrtrd.2	|- (ph -> BRC)

Assertion

Ref	Expression
eqbrtrd	|- (ph -> ARC)

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 |- (ph -> BRC)
2		eqbrtrd.1	. . 3 |- (ph -> A = B)
3	2	breq1d 2625	. 2 |- (ph -> (ARC <-> BRC))
4	1, 3	mpbird 196	1 |- (ph -> ARC)

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

This theorem is referenced by:  eqbrtrrd 2633  cdafi 4919  xrmin1 5869  xrmin2 5870  lbinfmle 6007  ceim1lt 6204  bernneq 6597  caure 6879  cauim 6880  faclbnd2 6898  faclbnd4lem3 6902  fsumcmp 6993  fsumabs2mul 6997  serzclim0 7062  climrecl 7063  climaddlem3 7069  climmullem4 7076  climmullem5 7077  climabslem 7101  climcau 7109  ser1cmp0 7128  cvgcmp3c 7139  cvgcmp3cetlem1 7141  reccnv 7170  georeclim 7192  geoisumr 7195  cvgratlem5 7206  mulc1cncf 7231  efaddlem10 7306  efaddlem11 7307  efaddlem16 7312  efaddlem17 7313  sin01bndlem3 7428  cos01bndlem3 7430  cos01gt0 7436  ruclem27 7496  alephsuc3 7545  metxplem4 7795  blcntr 7807  dscmet 7880  lmconst 7896  metcnp4lem2 7931  bcthlem20 7980  bcthlem21 7981  nvmtri2 8264  nvabs 8265  nvge0 8266  nvlmle 8296  sm1cnilem 8309  nmoubi 8395  nmblolbii 8418  blocnilem 8423  siii 8472  ubthlem3 8490  ubthlem10 8497  minveclem14 8517  minveclem21 8524  minveclem38 8541  htthlem6 8583  htthlem10 8587  bcsALT 9001  bcs3t 9005  projlem26 9166  nmopubt 9789  nmfnleubt 9806  nmbdoplb 9905  nmcoplb 9914  nmophm 9917  nmbdfnlb 9934  nmcfnlb 9943  nlelch 9950  riesz1t 9954  cnlnadjlem2 9957  nmopadjle 9977  nmoptri 9983  nmopco 9984  nmopcoadj 9990  unierr 9993  branmfnt 9994  hmopidmchlem 10034  pjs14 10094  hstlet 10113  strlem3a 10135  cdj3lem2b 10320  mslb1 10545  msra3 10547

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