Theorem eqbrtrrd 4000

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

Syntax hints:   → wi 4   = wceq 1342   class class class wbr 3976

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 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-br 3977

This theorem is referenced by:  dftpos4  6222  phpm  6822  unsnfidcex  6876  fisseneq  6888  f1finf1o  6903  prmuloclemcalc  7497  mullocprlem  7502  cauappcvgprlemladdfl  7587  caucvgprlemopl  7601  caucvgprprlemloccalc  7616  caucvgprprlemopl  7629  ltadd1sr  7708  suplocsrlem  7740  axarch  7823  axpre-suploclemres  7833  lemulge11  8752  mul2lt0llt0  9688  mul2lt0lgt0  9689  mul2lt0pn  9691  xaddge0  9805  modqmuladdim  10292  ltexp2a  10497  leexp2a  10498  nnlesq  10548  faclbnd6  10646  facavg  10648  fiprsshashgt1  10719  cvg1nlemcxze  10910  resqrexlemover  10938  resqrexlemlo  10941  resqrexlemnmsq  10945  resqrexlemnm  10946  leabs  11002  abs3dif  11033  abs2dif  11034  maxabslemlub  11135  maxltsup  11146  bdtri  11167  xrmaxiflemab  11174  xrbdtri  11203  recn2  11244  imcn2  11245  iserex  11266  summodclem2a  11308  fsumge1  11388  isumrpcl  11421  cvgratnnlemseq  11453  cvgratnnlemsumlt  11455  mertenslemi1  11462  prodmodclem2a  11503  ege2le3  11598  efgt1p2  11622  efgt1p  11623  tanval2ap  11640  tanval3ap  11641  cos12dec  11694  eirraplem  11703  divalglemnqt  11842  mulgcd  11934  dvdssqlem  11948  nn0seqcvgd  11952  mulgcddvds  12005  rpdvds  12010  pw2dvdseulemle  12076  sqrt2irraplemnn  12088  qden1elz  12114  phimullem  12134  hashgcdlem  12147  hashgcdeq  12148  pceu  12204  pcdvdstr  12235  ennnfonelemex  12284  lmcn2  12821  psmetge0  12872  xmetge0  12906  cnopnap  13135  suplociccex  13144  ivthinclemlopn  13155  ivthinclemuopn  13157  cnplimclemr  13179  limccnp2lem  13186  dveflem  13228  efltlemlt  13236  cosq23lt0  13295  coseq0q4123  13296  cosq34lt1  13312  logdivlti  13343  apdiff  13761  taupi  13783