Theorem eqbrtrrd 4042

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

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4018

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-br 4019

This theorem is referenced by:  dftpos4  6289  phpm  6894  unsnfidcex  6949  fisseneq  6961  f1finf1o  6977  prmuloclemcalc  7595  mullocprlem  7600  cauappcvgprlemladdfl  7685  caucvgprlemopl  7699  caucvgprprlemloccalc  7714  caucvgprprlemopl  7727  ltadd1sr  7806  suplocsrlem  7838  axarch  7921  axpre-suploclemres  7931  lemulge11  8854  mul2lt0llt0  9793  mul2lt0lgt0  9794  mul2lt0pn  9796  xaddge0  9910  modqmuladdim  10400  ltexp2a  10606  leexp2a  10607  nnlesq  10658  faclbnd6  10759  facavg  10761  fiprsshashgt1  10832  cvg1nlemcxze  11026  resqrexlemover  11054  resqrexlemlo  11057  resqrexlemnmsq  11061  resqrexlemnm  11062  leabs  11118  abs3dif  11149  abs2dif  11150  maxabslemlub  11251  maxltsup  11262  bdtri  11283  xrmaxiflemab  11290  xrbdtri  11319  recn2  11360  imcn2  11361  iserex  11382  summodclem2a  11424  fsumge1  11504  isumrpcl  11537  cvgratnnlemseq  11569  cvgratnnlemsumlt  11571  mertenslemi1  11578  prodmodclem2a  11619  ege2le3  11714  efgt1p2  11738  efgt1p  11739  tanval2ap  11756  tanval3ap  11757  cos12dec  11810  eirraplem  11819  divalglemnqt  11960  mulgcd  12052  dvdssqlem  12066  nn0seqcvgd  12076  mulgcddvds  12129  rpdvds  12134  isprm5  12177  pw2dvdseulemle  12202  sqrt2irraplemnn  12214  qden1elz  12240  phimullem  12260  hashgcdlem  12273  hashgcdeq  12274  pceu  12330  pcdvdstr  12362  pockthg  12392  4sqlem11  12436  ennnfonelemex  12468  lmcn2  14257  psmetge0  14308  xmetge0  14342  cnopnap  14571  suplociccex  14580  ivthinclemlopn  14591  ivthinclemuopn  14593  cnplimclemr  14615  limccnp2lem  14622  dveflem  14664  efltlemlt  14672  cosq23lt0  14731  coseq0q4123  14732  cosq34lt1  14748  logdivlti  14779  lgsne0  14917  apdiff  15275  taupi  15300