Theorem eqbrtrrd 4067

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

Syntax hints:   → wi 4   = wceq 1372   class class class wbr 4043

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044

This theorem is referenced by:  dftpos4  6348  phpm  6961  unsnfidcex  7016  fisseneq  7030  f1finf1o  7048  prmuloclemcalc  7677  mullocprlem  7682  cauappcvgprlemladdfl  7767  caucvgprlemopl  7781  caucvgprprlemloccalc  7796  caucvgprprlemopl  7809  ltadd1sr  7888  suplocsrlem  7920  axarch  8003  axpre-suploclemres  8013  lemulge11  8938  mul2lt0llt0  9882  mul2lt0lgt0  9883  mul2lt0pn  9885  xaddge0  9999  modqmuladdim  10510  ltexp2a  10734  leexp2a  10735  nnlesq  10786  faclbnd6  10887  facavg  10889  fiprsshashgt1  10960  cvg1nlemcxze  11235  resqrexlemover  11263  resqrexlemlo  11266  resqrexlemnmsq  11270  resqrexlemnm  11271  leabs  11327  abs3dif  11358  abs2dif  11359  maxabslemlub  11460  maxltsup  11471  bdtri  11493  xrmaxiflemab  11500  xrbdtri  11529  recn2  11570  imcn2  11571  iserex  11592  summodclem2a  11634  fsumge1  11714  isumrpcl  11747  cvgratnnlemseq  11779  cvgratnnlemsumlt  11781  mertenslemi1  11788  prodmodclem2a  11829  ege2le3  11924  efgt1p2  11948  efgt1p  11949  tanval2ap  11966  tanval3ap  11967  cos12dec  12021  eirraplem  12030  fsumdvds  12095  divalglemnqt  12173  bitsfzo  12208  bitsmod  12209  bitscmp  12211  mulgcd  12279  dvdssqlem  12293  nn0seqcvgd  12305  mulgcddvds  12358  rpdvds  12363  isprm5  12406  pw2dvdseulemle  12431  sqrt2irraplemnn  12443  qden1elz  12469  phimullem  12489  hashgcdlem  12502  hashgcdeq  12504  pceu  12560  pcdvdstr  12592  pockthg  12622  4sqlem11  12666  ennnfonelemex  12727  znrrg  14364  lmcn2  14694  psmetge0  14745  xmetge0  14779  cnopnap  15025  suplociccex  15039  ivthinclemlopn  15050  ivthinclemuopn  15052  hoverb  15062  ivthdichlem  15065  cnplimclemr  15083  limccnp2lem  15090  dveflem  15140  efltlemlt  15188  cosq23lt0  15247  coseq0q4123  15248  cosq34lt1  15264  logdivlti  15295  lgsne0  15457  lgsquadlem1  15496  lgsquadlem2  15497  apdiff  15920  taupi  15945