Theorem eqbrtrrd 4078

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

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4054

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-br 4055

This theorem is referenced by:  dftpos4  6367  phpm  6983  unsnfidcex  7038  fisseneq  7052  f1finf1o  7070  prmuloclemcalc  7708  mullocprlem  7713  cauappcvgprlemladdfl  7798  caucvgprlemopl  7812  caucvgprprlemloccalc  7827  caucvgprprlemopl  7840  ltadd1sr  7919  suplocsrlem  7951  axarch  8034  axpre-suploclemres  8044  lemulge11  8969  mul2lt0llt0  9913  mul2lt0lgt0  9914  mul2lt0pn  9916  xaddge0  10030  modqmuladdim  10544  ltexp2a  10768  leexp2a  10769  nnlesq  10820  faclbnd6  10921  facavg  10923  fiprsshashgt1  10994  cvg1nlemcxze  11378  resqrexlemover  11406  resqrexlemlo  11409  resqrexlemnmsq  11413  resqrexlemnm  11414  leabs  11470  abs3dif  11501  abs2dif  11502  maxabslemlub  11603  maxltsup  11614  bdtri  11636  xrmaxiflemab  11643  xrbdtri  11672  recn2  11713  imcn2  11714  iserex  11735  summodclem2a  11777  fsumge1  11857  isumrpcl  11890  cvgratnnlemseq  11922  cvgratnnlemsumlt  11924  mertenslemi1  11931  prodmodclem2a  11972  ege2le3  12067  efgt1p2  12091  efgt1p  12092  tanval2ap  12109  tanval3ap  12110  cos12dec  12164  eirraplem  12173  fsumdvds  12238  divalglemnqt  12316  bitsfzo  12351  bitsmod  12352  bitscmp  12354  mulgcd  12422  dvdssqlem  12436  nn0seqcvgd  12448  mulgcddvds  12501  rpdvds  12506  isprm5  12549  pw2dvdseulemle  12574  sqrt2irraplemnn  12586  qden1elz  12612  phimullem  12632  hashgcdlem  12645  hashgcdeq  12647  pceu  12703  pcdvdstr  12735  pockthg  12765  4sqlem11  12809  ennnfonelemex  12870  znrrg  14507  lmcn2  14837  psmetge0  14888  xmetge0  14922  cnopnap  15168  suplociccex  15182  ivthinclemlopn  15193  ivthinclemuopn  15195  hoverb  15205  ivthdichlem  15208  cnplimclemr  15226  limccnp2lem  15233  dveflem  15283  efltlemlt  15331  cosq23lt0  15390  coseq0q4123  15391  cosq34lt1  15407  logdivlti  15438  lgsne0  15600  lgsquadlem1  15639  lgsquadlem2  15640  umgrnloopvv  15795  apdiff  16159  taupi  16184