Theorem eqbrtrrd 4110

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

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

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  dftpos4  6424  phpm  7047  unsnfidcex  7105  fisseneq  7119  f1finf1o  7137  prmuloclemcalc  7775  mullocprlem  7780  cauappcvgprlemladdfl  7865  caucvgprlemopl  7879  caucvgprprlemloccalc  7894  caucvgprprlemopl  7907  ltadd1sr  7986  suplocsrlem  8018  axarch  8101  axpre-suploclemres  8111  lemulge11  9036  mul2lt0llt0  9986  mul2lt0lgt0  9987  mul2lt0pn  9989  xaddge0  10103  modqmuladdim  10619  ltexp2a  10843  leexp2a  10844  nnlesq  10895  faclbnd6  10996  facavg  10998  fiprsshashgt1  11071  cvg1nlemcxze  11533  resqrexlemover  11561  resqrexlemlo  11564  resqrexlemnmsq  11568  resqrexlemnm  11569  leabs  11625  abs3dif  11656  abs2dif  11657  maxabslemlub  11758  maxltsup  11769  bdtri  11791  xrmaxiflemab  11798  xrbdtri  11827  recn2  11868  imcn2  11869  iserex  11890  summodclem2a  11932  fsumge1  12012  isumrpcl  12045  cvgratnnlemseq  12077  cvgratnnlemsumlt  12079  mertenslemi1  12086  prodmodclem2a  12127  ege2le3  12222  efgt1p2  12246  efgt1p  12247  tanval2ap  12264  tanval3ap  12265  cos12dec  12319  eirraplem  12328  fsumdvds  12393  divalglemnqt  12471  bitsfzo  12506  bitsmod  12507  bitscmp  12509  mulgcd  12577  dvdssqlem  12591  nn0seqcvgd  12603  mulgcddvds  12656  rpdvds  12661  isprm5  12704  pw2dvdseulemle  12729  sqrt2irraplemnn  12741  qden1elz  12767  phimullem  12787  hashgcdlem  12800  hashgcdeq  12802  pceu  12858  pcdvdstr  12890  pockthg  12920  4sqlem11  12964  ennnfonelemex  13025  znrrg  14664  lmcn2  14994  psmetge0  15045  xmetge0  15079  cnopnap  15325  suplociccex  15339  ivthinclemlopn  15350  ivthinclemuopn  15352  hoverb  15362  ivthdichlem  15365  cnplimclemr  15383  limccnp2lem  15390  dveflem  15440  efltlemlt  15488  cosq23lt0  15547  coseq0q4123  15548  cosq34lt1  15564  logdivlti  15595  lgsne0  15757  lgsquadlem1  15796  lgsquadlem2  15797  umgrnloopv  15955  umgredgprv  15956  apdiff  16588  taupi  16613