Theorem eqbrtrrd 4014

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

Syntax hints:   → wi 4   = wceq 1349   class class class wbr 3990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-v 2733  df-un 3126  df-sn 3590  df-pr 3591  df-op 3593  df-br 3991

This theorem is referenced by:  dftpos4  6246  phpm  6847  unsnfidcex  6901  fisseneq  6913  f1finf1o  6928  prmuloclemcalc  7531  mullocprlem  7536  cauappcvgprlemladdfl  7621  caucvgprlemopl  7635  caucvgprprlemloccalc  7650  caucvgprprlemopl  7663  ltadd1sr  7742  suplocsrlem  7774  axarch  7857  axpre-suploclemres  7867  lemulge11  8786  mul2lt0llt0  9722  mul2lt0lgt0  9723  mul2lt0pn  9725  xaddge0  9839  modqmuladdim  10327  ltexp2a  10532  leexp2a  10533  nnlesq  10583  faclbnd6  10682  facavg  10684  fiprsshashgt1  10756  cvg1nlemcxze  10950  resqrexlemover  10978  resqrexlemlo  10981  resqrexlemnmsq  10985  resqrexlemnm  10986  leabs  11042  abs3dif  11073  abs2dif  11074  maxabslemlub  11175  maxltsup  11186  bdtri  11207  xrmaxiflemab  11214  xrbdtri  11243  recn2  11284  imcn2  11285  iserex  11306  summodclem2a  11348  fsumge1  11428  isumrpcl  11461  cvgratnnlemseq  11493  cvgratnnlemsumlt  11495  mertenslemi1  11502  prodmodclem2a  11543  ege2le3  11638  efgt1p2  11662  efgt1p  11663  tanval2ap  11680  tanval3ap  11681  cos12dec  11734  eirraplem  11743  divalglemnqt  11883  mulgcd  11975  dvdssqlem  11989  nn0seqcvgd  11999  mulgcddvds  12052  rpdvds  12057  isprm5  12100  pw2dvdseulemle  12125  sqrt2irraplemnn  12137  qden1elz  12163  phimullem  12183  hashgcdlem  12196  hashgcdeq  12197  pceu  12253  pcdvdstr  12284  pockthg  12313  ennnfonelemex  12373  lmcn2  13159  psmetge0  13210  xmetge0  13244  cnopnap  13473  suplociccex  13482  ivthinclemlopn  13493  ivthinclemuopn  13495  cnplimclemr  13517  limccnp2lem  13524  dveflem  13566  efltlemlt  13574  cosq23lt0  13633  coseq0q4123  13634  cosq34lt1  13650  logdivlti  13681  lgsne0  13818  apdiff  14165  taupi  14187