Theorem eqbrtrrd 3952

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

Syntax hints:   → wi 4   = wceq 1331   class class class wbr 3929

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930

This theorem is referenced by:  dftpos4  6160  phpm  6759  unsnfidcex  6808  fisseneq  6820  f1finf1o  6835  prmuloclemcalc  7373  mullocprlem  7378  cauappcvgprlemladdfl  7463  caucvgprlemopl  7477  caucvgprprlemloccalc  7492  caucvgprprlemopl  7505  ltadd1sr  7584  suplocsrlem  7616  axarch  7699  axpre-suploclemres  7709  lemulge11  8624  mul2lt0llt0  9548  mul2lt0lgt0  9549  mul2lt0pn  9551  xaddge0  9661  modqmuladdim  10140  ltexp2a  10345  leexp2a  10346  nnlesq  10396  faclbnd6  10490  facavg  10492  fiprsshashgt1  10563  cvg1nlemcxze  10754  resqrexlemover  10782  resqrexlemlo  10785  resqrexlemnmsq  10789  resqrexlemnm  10790  leabs  10846  abs3dif  10877  abs2dif  10878  maxabslemlub  10979  maxltsup  10990  bdtri  11011  xrmaxiflemab  11016  xrbdtri  11045  recn2  11086  imcn2  11087  iserex  11108  summodclem2a  11150  fsumge1  11230  isumrpcl  11263  cvgratnnlemseq  11295  cvgratnnlemsumlt  11297  mertenslemi1  11304  prodmodclem2a  11345  ege2le3  11377  efgt1p2  11401  efgt1p  11402  tanval2ap  11420  tanval3ap  11421  cos12dec  11474  eirraplem  11483  divalglemnqt  11617  mulgcd  11704  dvdssqlem  11718  nn0seqcvgd  11722  mulgcddvds  11775  rpdvds  11780  pw2dvdseulemle  11845  sqrt2irraplemnn  11857  qden1elz  11883  phimullem  11901  hashgcdlem  11903  hashgcdeq  11904  ennnfonelemex  11927  lmcn2  12449  psmetge0  12500  xmetge0  12534  cnopnap  12763  suplociccex  12772  ivthinclemlopn  12783  ivthinclemuopn  12785  cnplimclemr  12807  limccnp2lem  12814  dveflem  12855  cosq23lt0  12914  coseq0q4123  12915  cosq34lt1  12931  taupi  13239