Theorem eqbrtrrd 4068

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

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4044

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4045

This theorem is referenced by:  dftpos4  6349  phpm  6962  unsnfidcex  7017  fisseneq  7031  f1finf1o  7049  prmuloclemcalc  7678  mullocprlem  7683  cauappcvgprlemladdfl  7768  caucvgprlemopl  7782  caucvgprprlemloccalc  7797  caucvgprprlemopl  7810  ltadd1sr  7889  suplocsrlem  7921  axarch  8004  axpre-suploclemres  8014  lemulge11  8939  mul2lt0llt0  9883  mul2lt0lgt0  9884  mul2lt0pn  9886  xaddge0  10000  modqmuladdim  10512  ltexp2a  10736  leexp2a  10737  nnlesq  10788  faclbnd6  10889  facavg  10891  fiprsshashgt1  10962  cvg1nlemcxze  11293  resqrexlemover  11321  resqrexlemlo  11324  resqrexlemnmsq  11328  resqrexlemnm  11329  leabs  11385  abs3dif  11416  abs2dif  11417  maxabslemlub  11518  maxltsup  11529  bdtri  11551  xrmaxiflemab  11558  xrbdtri  11587  recn2  11628  imcn2  11629  iserex  11650  summodclem2a  11692  fsumge1  11772  isumrpcl  11805  cvgratnnlemseq  11837  cvgratnnlemsumlt  11839  mertenslemi1  11846  prodmodclem2a  11887  ege2le3  11982  efgt1p2  12006  efgt1p  12007  tanval2ap  12024  tanval3ap  12025  cos12dec  12079  eirraplem  12088  fsumdvds  12153  divalglemnqt  12231  bitsfzo  12266  bitsmod  12267  bitscmp  12269  mulgcd  12337  dvdssqlem  12351  nn0seqcvgd  12363  mulgcddvds  12416  rpdvds  12421  isprm5  12464  pw2dvdseulemle  12489  sqrt2irraplemnn  12501  qden1elz  12527  phimullem  12547  hashgcdlem  12560  hashgcdeq  12562  pceu  12618  pcdvdstr  12650  pockthg  12680  4sqlem11  12724  ennnfonelemex  12785  znrrg  14422  lmcn2  14752  psmetge0  14803  xmetge0  14837  cnopnap  15083  suplociccex  15097  ivthinclemlopn  15108  ivthinclemuopn  15110  hoverb  15120  ivthdichlem  15123  cnplimclemr  15141  limccnp2lem  15148  dveflem  15198  efltlemlt  15246  cosq23lt0  15305  coseq0q4123  15306  cosq34lt1  15322  logdivlti  15353  lgsne0  15515  lgsquadlem1  15554  lgsquadlem2  15555  apdiff  15987  taupi  16012