Theorem eqbrtrrd 4067

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

Syntax hints:   → wi 4   = wceq 1372   class class class wbr 4043

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044

This theorem is referenced by:  dftpos4  6348  phpm  6961  unsnfidcex  7016  fisseneq  7030  f1finf1o  7048  prmuloclemcalc  7677  mullocprlem  7682  cauappcvgprlemladdfl  7767  caucvgprlemopl  7781  caucvgprprlemloccalc  7796  caucvgprprlemopl  7809  ltadd1sr  7888  suplocsrlem  7920  axarch  8003  axpre-suploclemres  8013  lemulge11  8938  mul2lt0llt0  9882  mul2lt0lgt0  9883  mul2lt0pn  9885  xaddge0  9999  modqmuladdim  10510  ltexp2a  10734  leexp2a  10735  nnlesq  10786  faclbnd6  10887  facavg  10889  fiprsshashgt1  10960  cvg1nlemcxze  11264  resqrexlemover  11292  resqrexlemlo  11295  resqrexlemnmsq  11299  resqrexlemnm  11300  leabs  11356  abs3dif  11387  abs2dif  11388  maxabslemlub  11489  maxltsup  11500  bdtri  11522  xrmaxiflemab  11529  xrbdtri  11558  recn2  11599  imcn2  11600  iserex  11621  summodclem2a  11663  fsumge1  11743  isumrpcl  11776  cvgratnnlemseq  11808  cvgratnnlemsumlt  11810  mertenslemi1  11817  prodmodclem2a  11858  ege2le3  11953  efgt1p2  11977  efgt1p  11978  tanval2ap  11995  tanval3ap  11996  cos12dec  12050  eirraplem  12059  fsumdvds  12124  divalglemnqt  12202  bitsfzo  12237  bitsmod  12238  bitscmp  12240  mulgcd  12308  dvdssqlem  12322  nn0seqcvgd  12334  mulgcddvds  12387  rpdvds  12392  isprm5  12435  pw2dvdseulemle  12460  sqrt2irraplemnn  12472  qden1elz  12498  phimullem  12518  hashgcdlem  12531  hashgcdeq  12533  pceu  12589  pcdvdstr  12621  pockthg  12651  4sqlem11  12695  ennnfonelemex  12756  znrrg  14393  lmcn2  14723  psmetge0  14774  xmetge0  14808  cnopnap  15054  suplociccex  15068  ivthinclemlopn  15079  ivthinclemuopn  15081  hoverb  15091  ivthdichlem  15094  cnplimclemr  15112  limccnp2lem  15119  dveflem  15169  efltlemlt  15217  cosq23lt0  15276  coseq0q4123  15277  cosq34lt1  15293  logdivlti  15324  lgsne0  15486  lgsquadlem1  15525  lgsquadlem2  15526  apdiff  15949  taupi  15974