Theorem eqbrtrrd 4154

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  dftpos4  6534  phpm  7167  unsnfidcex  7227  fisseneq  7242  f1finf1o  7264  prmuloclemcalc  7932  mullocprlem  7937  cauappcvgprlemladdfl  8022  caucvgprlemopl  8036  caucvgprprlemloccalc  8051  caucvgprprlemopl  8064  ltadd1sr  8143  suplocsrlem  8175  axarch  8258  axpre-suploclemres  8268  lemulge11  9196  mul2lt0llt0  10162  mul2lt0lgt0  10163  mul2lt0pn  10165  xaddge0  10280  modqmuladdim  10804  ltexp2a  11028  leexp2a  11029  nnlesq  11080  faclbnd6  11182  facavg  11184  bcm1n  11207  fiprsshashgt1  11258  sseqn  11279  sq01  11660  cvg1nlemcxze  11748  resqrexlemover  11776  resqrexlemlo  11779  resqrexlemnmsq  11783  resqrexlemnm  11784  leabs  11840  abs3dif  11871  abs2dif  11872  maxabslemlub  11973  maxltsup  11984  bdtri  12006  xrmaxiflemab  12013  xrbdtri  12042  recn2  12083  imcn2  12084  iserex  12105  summodclem2a  12148  fsumge1  12228  isumrpcl  12261  cvgratnnlemseq  12293  cvgratnnlemsumlt  12295  mertenslemi1  12302  prodmodclem2a  12343  ege2le3  12438  efgt1p2  12462  efgt1p  12463  tanval2ap  12480  tanval3ap  12481  cos12dec  12535  eirraplem  12544  fsumdvds  12609  divalglemnqt  12687  bitsfzo  12722  bitsmod  12723  bitscmp  12725  mulgcd  12793  dvdssqlem  12807  nn0seqcvgd  12819  mulgcddvds  12872  rpdvds  12877  isprm5  12920  pw2dvdseulemle  12945  sqrt2irraplemnn  12957  qden1elz  12983  phimullem  13003  hashgcdlem  13016  hashgcdeq  13018  pceu  13074  pcdvdstr  13106  pockthg  13136  4sqlem11  13180  ennnfonelemex  13305  znrrg  14995  lmcn2  15381  psmetge0  15432  xmetge0  15466  cnopnap  15712  suplociccex  15726  ivthinclemlopn  15737  ivthinclemuopn  15739  hoverb  15749  ivthdichlem  15752  cnplimclemr  15770  limccnp2lem  15777  dveflem  15827  efltlemlt  15875  cosq23lt0  15934  coseq0q4123  15935  cosq34lt1  15951  logdivlti  15982  lgsne0  16157  lgsquadlem1  16196  lgsquadlem2  16197  umgrnloopv  16355  umgredgprv  16356  upgr1een  16365  1hegrvtxdg1fi  16550  apdiff  17097  taupi  17123