Theorem eqbrtrrd 4058

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  dftpos4  6330  phpm  6935  unsnfidcex  6990  fisseneq  7004  f1finf1o  7022  prmuloclemcalc  7651  mullocprlem  7656  cauappcvgprlemladdfl  7741  caucvgprlemopl  7755  caucvgprprlemloccalc  7770  caucvgprprlemopl  7783  ltadd1sr  7862  suplocsrlem  7894  axarch  7977  axpre-suploclemres  7987  lemulge11  8912  mul2lt0llt0  9855  mul2lt0lgt0  9856  mul2lt0pn  9858  xaddge0  9972  modqmuladdim  10478  ltexp2a  10702  leexp2a  10703  nnlesq  10754  faclbnd6  10855  facavg  10857  fiprsshashgt1  10928  cvg1nlemcxze  11166  resqrexlemover  11194  resqrexlemlo  11197  resqrexlemnmsq  11201  resqrexlemnm  11202  leabs  11258  abs3dif  11289  abs2dif  11290  maxabslemlub  11391  maxltsup  11402  bdtri  11424  xrmaxiflemab  11431  xrbdtri  11460  recn2  11501  imcn2  11502  iserex  11523  summodclem2a  11565  fsumge1  11645  isumrpcl  11678  cvgratnnlemseq  11710  cvgratnnlemsumlt  11712  mertenslemi1  11719  prodmodclem2a  11760  ege2le3  11855  efgt1p2  11879  efgt1p  11880  tanval2ap  11897  tanval3ap  11898  cos12dec  11952  eirraplem  11961  fsumdvds  12026  divalglemnqt  12104  bitsfzo  12139  bitsmod  12140  bitscmp  12142  mulgcd  12210  dvdssqlem  12224  nn0seqcvgd  12236  mulgcddvds  12289  rpdvds  12294  isprm5  12337  pw2dvdseulemle  12362  sqrt2irraplemnn  12374  qden1elz  12400  phimullem  12420  hashgcdlem  12433  hashgcdeq  12435  pceu  12491  pcdvdstr  12523  pockthg  12553  4sqlem11  12597  ennnfonelemex  12658  znrrg  14294  lmcn2  14624  psmetge0  14675  xmetge0  14709  cnopnap  14955  suplociccex  14969  ivthinclemlopn  14980  ivthinclemuopn  14982  hoverb  14992  ivthdichlem  14995  cnplimclemr  15013  limccnp2lem  15020  dveflem  15070  efltlemlt  15118  cosq23lt0  15177  coseq0q4123  15178  cosq34lt1  15194  logdivlti  15225  lgsne0  15387  lgsquadlem1  15426  lgsquadlem2  15427  apdiff  15805  taupi  15830