Theorem eqbrtrrd 4053

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

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

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 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  dftpos4  6316  phpm  6921  unsnfidcex  6976  fisseneq  6988  f1finf1o  7006  prmuloclemcalc  7625  mullocprlem  7630  cauappcvgprlemladdfl  7715  caucvgprlemopl  7729  caucvgprprlemloccalc  7744  caucvgprprlemopl  7757  ltadd1sr  7836  suplocsrlem  7868  axarch  7951  axpre-suploclemres  7961  lemulge11  8885  mul2lt0llt0  9827  mul2lt0lgt0  9828  mul2lt0pn  9830  xaddge0  9944  modqmuladdim  10438  ltexp2a  10662  leexp2a  10663  nnlesq  10714  faclbnd6  10815  facavg  10817  fiprsshashgt1  10888  cvg1nlemcxze  11126  resqrexlemover  11154  resqrexlemlo  11157  resqrexlemnmsq  11161  resqrexlemnm  11162  leabs  11218  abs3dif  11249  abs2dif  11250  maxabslemlub  11351  maxltsup  11362  bdtri  11383  xrmaxiflemab  11390  xrbdtri  11419  recn2  11460  imcn2  11461  iserex  11482  summodclem2a  11524  fsumge1  11604  isumrpcl  11637  cvgratnnlemseq  11669  cvgratnnlemsumlt  11671  mertenslemi1  11678  prodmodclem2a  11719  ege2le3  11814  efgt1p2  11838  efgt1p  11839  tanval2ap  11856  tanval3ap  11857  cos12dec  11911  eirraplem  11920  divalglemnqt  12061  mulgcd  12153  dvdssqlem  12167  nn0seqcvgd  12179  mulgcddvds  12232  rpdvds  12237  isprm5  12280  pw2dvdseulemle  12305  sqrt2irraplemnn  12317  qden1elz  12343  phimullem  12363  hashgcdlem  12376  hashgcdeq  12377  pceu  12433  pcdvdstr  12465  pockthg  12495  4sqlem11  12539  ennnfonelemex  12571  znrrg  14148  lmcn2  14448  psmetge0  14499  xmetge0  14533  cnopnap  14765  suplociccex  14779  ivthinclemlopn  14790  ivthinclemuopn  14792  hoverb  14802  ivthdichlem  14805  cnplimclemr  14823  limccnp2lem  14830  dveflem  14872  efltlemlt  14909  cosq23lt0  14968  coseq0q4123  14969  cosq34lt1  14985  logdivlti  15016  lgsne0  15154  lgsquadlem1  15191  apdiff  15538  taupi  15563