Theorem eqbrtrrd 4155

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 4153	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

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

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 4132

This theorem is used by:  dftpos4  6539  phpm  7173  unsnfidcex  7233  fisseneq  7248  f1finf1o  7271  prmuloclemcalc  7938  mullocprlem  7943  cauappcvgprlemladdfl  8028  caucvgprlemopl  8042  caucvgprprlemloccalc  8057  caucvgprprlemopl  8070  ltadd1sr  8149  suplocsrlem  8181  axarch  8264  axpre-suploclemres  8274  lemulge11  9204  mul2lt0llt0  10178  mul2lt0lgt0  10179  mul2lt0pn  10181  xaddge0  10296  modqmuladdim  10824  ltexp2a  11048  leexp2a  11049  nnlesq  11100  faclbnd6  11203  facavg  11205  bcm1n  11228  fiprsshashgt1  11279  sseqn  11300  sq01  11681  cvg1nlemcxze  11769  resqrexlemover  11797  resqrexlemlo  11800  resqrexlemnmsq  11804  resqrexlemnm  11805  leabs  11861  abs3dif  11893  abs2dif  11894  maxabslemlub  11995  maxltsup  12006  bdtri  12030  xrmaxiflemab  12037  xrbdtri  12066  recn2  12107  imcn2  12108  iserex  12129  summodclem2a  12172  fsumge1  12252  isumrpcl  12285  cvgratnnlemseq  12317  cvgratnnlemsumlt  12319  mertenslemi1  12326  prodmodclem2a  12367  ege2le3  12462  efgt1p2  12486  efgt1p  12487  tanval2ap  12504  tanval3ap  12505  cos12dec  12559  eirraplem  12568  fsumdvds  12633  divalglemnqt  12711  bitsfzo  12746  bitsmod  12747  bitscmp  12749  mulgcd  12817  dvdssqlem  12831  nn0seqcvgd  12843  mulgcddvds  12896  rpdvds  12901  isprm5  12945  pwbdvdseulemle  12970  sqrt2irraplemnn  12983  qden1elz  13009  phimullem  13031  hashgcdlem  13044  hashgcdeq  13046  pceu  13102  pcdvdstr  13134  pockthg  13164  4sqlem11  13208  ennnfonelemex  13362  znrrg  15103  lmcn2  15523  psmetge0  15574  xmetge0  15608  cnopnap  15854  suplociccex  15868  ivthinclemlopn  15879  ivthinclemuopn  15881  hoverb  15891  ivthdichlem  15894  cnplimclemr  15912  limccnp2lem  15919  dveflem  15969  efltlemlt  16017  cosq23lt0  16077  coseq0q4123  16078  cosq34lt1  16095  logdivlti  16128  logdivlt  16141  ppiqltx  16298  chtqub  16313  bcmono  16321  bposlem2  16329  bposlem5  16332  bposlem6  16333  lgsne0  16379  lgsquadlem1  16418  lgsquadlem2  16419  umgrnloopv  16577  umgredgprv  16578  upgr1een  16587  1hegrvtxdg1fi  16772  apdiff  17321  taupi  17347