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  7933  mullocprlem  7938  cauappcvgprlemladdfl  8023  caucvgprlemopl  8037  caucvgprprlemloccalc  8052  caucvgprprlemopl  8065  ltadd1sr  8144  suplocsrlem  8176  axarch  8259  axpre-suploclemres  8269  lemulge11  9199  mul2lt0llt0  10173  mul2lt0lgt0  10174  mul2lt0pn  10176  xaddge0  10291  modqmuladdim  10819  ltexp2a  11043  leexp2a  11044  nnlesq  11095  faclbnd6  11198  facavg  11200  bcm1n  11223  fiprsshashgt1  11274  sseqn  11295  sq01  11676  cvg1nlemcxze  11764  resqrexlemover  11792  resqrexlemlo  11795  resqrexlemnmsq  11799  resqrexlemnm  11800  leabs  11856  abs3dif  11888  abs2dif  11889  maxabslemlub  11990  maxltsup  12001  bdtri  12025  xrmaxiflemab  12032  xrbdtri  12061  recn2  12102  imcn2  12103  iserex  12124  summodclem2a  12167  fsumge1  12247  isumrpcl  12280  cvgratnnlemseq  12312  cvgratnnlemsumlt  12314  mertenslemi1  12321  prodmodclem2a  12362  ege2le3  12457  efgt1p2  12481  efgt1p  12482  tanval2ap  12499  tanval3ap  12500  cos12dec  12554  eirraplem  12563  fsumdvds  12628  divalglemnqt  12706  bitsfzo  12741  bitsmod  12742  bitscmp  12744  mulgcd  12812  dvdssqlem  12826  nn0seqcvgd  12838  mulgcddvds  12891  rpdvds  12896  isprm5  12940  pwbdvdseulemle  12965  sqrt2irraplemnn  12978  qden1elz  13004  phimullem  13026  hashgcdlem  13039  hashgcdeq  13041  pceu  13097  pcdvdstr  13129  pockthg  13159  4sqlem11  13203  ennnfonelemex  13357  znrrg  15079  lmcn2  15472  psmetge0  15523  xmetge0  15557  cnopnap  15803  suplociccex  15817  ivthinclemlopn  15828  ivthinclemuopn  15830  hoverb  15840  ivthdichlem  15843  cnplimclemr  15861  limccnp2lem  15868  dveflem  15918  efltlemlt  15966  cosq23lt0  16026  coseq0q4123  16027  cosq34lt1  16043  logdivlti  16075  logdivlt  16088  ppiqltx  16242  chtqub  16257  bcmono  16265  bposlem2  16273  bposlem5  16276  bposlem6  16277  lgsne0  16323  lgsquadlem1  16362  lgsquadlem2  16363  umgrnloopv  16521  umgredgprv  16522  upgr1een  16531  1hegrvtxdg1fi  16716  apdiff  17264  taupi  17290