Theorem eqbrtrrd 4107

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

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  dftpos4  6415  phpm  7035  unsnfidcex  7093  fisseneq  7107  f1finf1o  7125  prmuloclemcalc  7763  mullocprlem  7768  cauappcvgprlemladdfl  7853  caucvgprlemopl  7867  caucvgprprlemloccalc  7882  caucvgprprlemopl  7895  ltadd1sr  7974  suplocsrlem  8006  axarch  8089  axpre-suploclemres  8099  lemulge11  9024  mul2lt0llt0  9969  mul2lt0lgt0  9970  mul2lt0pn  9972  xaddge0  10086  modqmuladdim  10601  ltexp2a  10825  leexp2a  10826  nnlesq  10877  faclbnd6  10978  facavg  10980  fiprsshashgt1  11052  cvg1nlemcxze  11508  resqrexlemover  11536  resqrexlemlo  11539  resqrexlemnmsq  11543  resqrexlemnm  11544  leabs  11600  abs3dif  11631  abs2dif  11632  maxabslemlub  11733  maxltsup  11744  bdtri  11766  xrmaxiflemab  11773  xrbdtri  11802  recn2  11843  imcn2  11844  iserex  11865  summodclem2a  11907  fsumge1  11987  isumrpcl  12020  cvgratnnlemseq  12052  cvgratnnlemsumlt  12054  mertenslemi1  12061  prodmodclem2a  12102  ege2le3  12197  efgt1p2  12221  efgt1p  12222  tanval2ap  12239  tanval3ap  12240  cos12dec  12294  eirraplem  12303  fsumdvds  12368  divalglemnqt  12446  bitsfzo  12481  bitsmod  12482  bitscmp  12484  mulgcd  12552  dvdssqlem  12566  nn0seqcvgd  12578  mulgcddvds  12631  rpdvds  12636  isprm5  12679  pw2dvdseulemle  12704  sqrt2irraplemnn  12716  qden1elz  12742  phimullem  12762  hashgcdlem  12775  hashgcdeq  12777  pceu  12833  pcdvdstr  12865  pockthg  12895  4sqlem11  12939  ennnfonelemex  13000  znrrg  14639  lmcn2  14969  psmetge0  15020  xmetge0  15054  cnopnap  15300  suplociccex  15314  ivthinclemlopn  15325  ivthinclemuopn  15327  hoverb  15337  ivthdichlem  15340  cnplimclemr  15358  limccnp2lem  15365  dveflem  15415  efltlemlt  15463  cosq23lt0  15522  coseq0q4123  15523  cosq34lt1  15539  logdivlti  15570  lgsne0  15732  lgsquadlem1  15771  lgsquadlem2  15772  umgrnloopv  15929  umgredgprv  15930  apdiff  16476  taupi  16501