Theorem eqbrtrrd 4022

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 2181	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 4020	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 3998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999

This theorem is referenced by:  dftpos4  6254  phpm  6855  unsnfidcex  6909  fisseneq  6921  f1finf1o  6936  prmuloclemcalc  7539  mullocprlem  7544  cauappcvgprlemladdfl  7629  caucvgprlemopl  7643  caucvgprprlemloccalc  7658  caucvgprprlemopl  7671  ltadd1sr  7750  suplocsrlem  7782  axarch  7865  axpre-suploclemres  7875  lemulge11  8794  mul2lt0llt0  9730  mul2lt0lgt0  9731  mul2lt0pn  9733  xaddge0  9847  modqmuladdim  10335  ltexp2a  10540  leexp2a  10541  nnlesq  10591  faclbnd6  10690  facavg  10692  fiprsshashgt1  10763  cvg1nlemcxze  10957  resqrexlemover  10985  resqrexlemlo  10988  resqrexlemnmsq  10992  resqrexlemnm  10993  leabs  11049  abs3dif  11080  abs2dif  11081  maxabslemlub  11182  maxltsup  11193  bdtri  11214  xrmaxiflemab  11221  xrbdtri  11250  recn2  11291  imcn2  11292  iserex  11313  summodclem2a  11355  fsumge1  11435  isumrpcl  11468  cvgratnnlemseq  11500  cvgratnnlemsumlt  11502  mertenslemi1  11509  prodmodclem2a  11550  ege2le3  11645  efgt1p2  11669  efgt1p  11670  tanval2ap  11687  tanval3ap  11688  cos12dec  11741  eirraplem  11750  divalglemnqt  11890  mulgcd  11982  dvdssqlem  11996  nn0seqcvgd  12006  mulgcddvds  12059  rpdvds  12064  isprm5  12107  pw2dvdseulemle  12132  sqrt2irraplemnn  12144  qden1elz  12170  phimullem  12190  hashgcdlem  12203  hashgcdeq  12204  pceu  12260  pcdvdstr  12291  pockthg  12320  ennnfonelemex  12380  lmcn2  13331  psmetge0  13382  xmetge0  13416  cnopnap  13645  suplociccex  13654  ivthinclemlopn  13665  ivthinclemuopn  13667  cnplimclemr  13689  limccnp2lem  13696  dveflem  13738  efltlemlt  13746  cosq23lt0  13805  coseq0q4123  13806  cosq34lt1  13822  logdivlti  13853  lgsne0  13990  apdiff  14337  taupi  14359