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  6429  phpm  7052  unsnfidcex  7112  fisseneq  7127  f1finf1o  7146  prmuloclemcalc  7785  mullocprlem  7790  cauappcvgprlemladdfl  7875  caucvgprlemopl  7889  caucvgprprlemloccalc  7904  caucvgprprlemopl  7917  ltadd1sr  7996  suplocsrlem  8028  axarch  8111  axpre-suploclemres  8121  lemulge11  9046  mul2lt0llt0  9996  mul2lt0lgt0  9997  mul2lt0pn  9999  xaddge0  10113  modqmuladdim  10630  ltexp2a  10854  leexp2a  10855  nnlesq  10906  faclbnd6  11007  facavg  11009  fiprsshashgt1  11082  cvg1nlemcxze  11560  resqrexlemover  11588  resqrexlemlo  11591  resqrexlemnmsq  11595  resqrexlemnm  11596  leabs  11652  abs3dif  11683  abs2dif  11684  maxabslemlub  11785  maxltsup  11796  bdtri  11818  xrmaxiflemab  11825  xrbdtri  11854  recn2  11895  imcn2  11896  iserex  11917  summodclem2a  11960  fsumge1  12040  isumrpcl  12073  cvgratnnlemseq  12105  cvgratnnlemsumlt  12107  mertenslemi1  12114  prodmodclem2a  12155  ege2le3  12250  efgt1p2  12274  efgt1p  12275  tanval2ap  12292  tanval3ap  12293  cos12dec  12347  eirraplem  12356  fsumdvds  12421  divalglemnqt  12499  bitsfzo  12534  bitsmod  12535  bitscmp  12537  mulgcd  12605  dvdssqlem  12619  nn0seqcvgd  12631  mulgcddvds  12684  rpdvds  12689  isprm5  12732  pw2dvdseulemle  12757  sqrt2irraplemnn  12769  qden1elz  12795  phimullem  12815  hashgcdlem  12828  hashgcdeq  12830  pceu  12886  pcdvdstr  12918  pockthg  12948  4sqlem11  12992  ennnfonelemex  13053  znrrg  14693  lmcn2  15023  psmetge0  15074  xmetge0  15108  cnopnap  15354  suplociccex  15368  ivthinclemlopn  15379  ivthinclemuopn  15381  hoverb  15391  ivthdichlem  15394  cnplimclemr  15412  limccnp2lem  15419  dveflem  15469  efltlemlt  15517  cosq23lt0  15576  coseq0q4123  15577  cosq34lt1  15593  logdivlti  15624  lgsne0  15786  lgsquadlem1  15825  lgsquadlem2  15826  umgrnloopv  15984  umgredgprv  15985  upgr1een  15994  1hegrvtxdg1fi  16179  apdiff  16703  taupi  16729