Theorem eqbrtrrd 4112

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

Syntax hints:   → wi 4   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  dftpos4  6428  phpm  7051  unsnfidcex  7111  fisseneq  7126  f1finf1o  7145  prmuloclemcalc  7784  mullocprlem  7789  cauappcvgprlemladdfl  7874  caucvgprlemopl  7888  caucvgprprlemloccalc  7903  caucvgprprlemopl  7916  ltadd1sr  7995  suplocsrlem  8027  axarch  8110  axpre-suploclemres  8120  lemulge11  9045  mul2lt0llt0  9995  mul2lt0lgt0  9996  mul2lt0pn  9998  xaddge0  10112  modqmuladdim  10628  ltexp2a  10852  leexp2a  10853  nnlesq  10904  faclbnd6  11005  facavg  11007  fiprsshashgt1  11080  cvg1nlemcxze  11542  resqrexlemover  11570  resqrexlemlo  11573  resqrexlemnmsq  11577  resqrexlemnm  11578  leabs  11634  abs3dif  11665  abs2dif  11666  maxabslemlub  11767  maxltsup  11778  bdtri  11800  xrmaxiflemab  11807  xrbdtri  11836  recn2  11877  imcn2  11878  iserex  11899  summodclem2a  11941  fsumge1  12021  isumrpcl  12054  cvgratnnlemseq  12086  cvgratnnlemsumlt  12088  mertenslemi1  12095  prodmodclem2a  12136  ege2le3  12231  efgt1p2  12255  efgt1p  12256  tanval2ap  12273  tanval3ap  12274  cos12dec  12328  eirraplem  12337  fsumdvds  12402  divalglemnqt  12480  bitsfzo  12515  bitsmod  12516  bitscmp  12518  mulgcd  12586  dvdssqlem  12600  nn0seqcvgd  12612  mulgcddvds  12665  rpdvds  12670  isprm5  12713  pw2dvdseulemle  12738  sqrt2irraplemnn  12750  qden1elz  12776  phimullem  12796  hashgcdlem  12809  hashgcdeq  12811  pceu  12867  pcdvdstr  12899  pockthg  12929  4sqlem11  12973  ennnfonelemex  13034  znrrg  14673  lmcn2  15003  psmetge0  15054  xmetge0  15088  cnopnap  15334  suplociccex  15348  ivthinclemlopn  15359  ivthinclemuopn  15361  hoverb  15371  ivthdichlem  15374  cnplimclemr  15392  limccnp2lem  15399  dveflem  15449  efltlemlt  15497  cosq23lt0  15556  coseq0q4123  15557  cosq34lt1  15573  logdivlti  15604  lgsne0  15766  lgsquadlem1  15805  lgsquadlem2  15806  umgrnloopv  15964  umgredgprv  15965  upgr1een  15974  1hegrvtxdg1fi  16159  apdiff  16652  taupi  16677