Theorem eqbrtrrd 4006

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqbrtrrd.2	⊢ (𝜑 → 𝐴𝑅𝐶)

Assertion

Ref	Expression
eqbrtrrd	⊢ (𝜑 → 𝐵𝑅𝐶)

Proof of Theorem eqbrtrrd

Step	Hyp	Ref	Expression
1		eqbrtrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2171	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 4004	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1343   class class class wbr 3982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-br 3983

This theorem is referenced by:  dftpos4  6231  phpm  6831  unsnfidcex  6885  fisseneq  6897  f1finf1o  6912  prmuloclemcalc  7506  mullocprlem  7511  cauappcvgprlemladdfl  7596  caucvgprlemopl  7610  caucvgprprlemloccalc  7625  caucvgprprlemopl  7638  ltadd1sr  7717  suplocsrlem  7749  axarch  7832  axpre-suploclemres  7842  lemulge11  8761  mul2lt0llt0  9697  mul2lt0lgt0  9698  mul2lt0pn  9700  xaddge0  9814  modqmuladdim  10302  ltexp2a  10507  leexp2a  10508  nnlesq  10558  faclbnd6  10657  facavg  10659  fiprsshashgt1  10730  cvg1nlemcxze  10924  resqrexlemover  10952  resqrexlemlo  10955  resqrexlemnmsq  10959  resqrexlemnm  10960  leabs  11016  abs3dif  11047  abs2dif  11048  maxabslemlub  11149  maxltsup  11160  bdtri  11181  xrmaxiflemab  11188  xrbdtri  11217  recn2  11258  imcn2  11259  iserex  11280  summodclem2a  11322  fsumge1  11402  isumrpcl  11435  cvgratnnlemseq  11467  cvgratnnlemsumlt  11469  mertenslemi1  11476  prodmodclem2a  11517  ege2le3  11612  efgt1p2  11636  efgt1p  11637  tanval2ap  11654  tanval3ap  11655  cos12dec  11708  eirraplem  11717  divalglemnqt  11857  mulgcd  11949  dvdssqlem  11963  nn0seqcvgd  11973  mulgcddvds  12026  rpdvds  12031  isprm5  12074  pw2dvdseulemle  12099  sqrt2irraplemnn  12111  qden1elz  12137  phimullem  12157  hashgcdlem  12170  hashgcdeq  12171  pceu  12227  pcdvdstr  12258  pockthg  12287  ennnfonelemex  12347  lmcn2  12920  psmetge0  12971  xmetge0  13005  cnopnap  13234  suplociccex  13243  ivthinclemlopn  13254  ivthinclemuopn  13256  cnplimclemr  13278  limccnp2lem  13285  dveflem  13327  efltlemlt  13335  cosq23lt0  13394  coseq0q4123  13395  cosq34lt1  13411  logdivlti  13442  lgsne0  13579  apdiff  13927  taupi  13949