Theorem eqbrtrrd 3842

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

Syntax hints:   → wi 4   = wceq 1287   class class class wbr 3820

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-br 3821

This theorem is referenced by:  dftpos4  5982  phpm  6533  unsnfidcex  6582  fisseneq  6592  f1finf1o  6605  prmuloclemcalc  7068  mullocprlem  7073  cauappcvgprlemladdfl  7158  caucvgprlemopl  7172  caucvgprprlemloccalc  7187  caucvgprprlemopl  7200  ltadd1sr  7266  axarch  7370  lemulge11  8262  modqmuladdim  9702  ltexp2a  9906  leexp2a  9907  nnlesq  9956  faclbnd6  10049  facavg  10051  fiprsshashgt1  10122  cvg1nlemcxze  10311  resqrexlemover  10339  resqrexlemlo  10342  resqrexlemnmsq  10346  resqrexlemnm  10347  leabs  10403  abs3dif  10434  abs2dif  10435  maxabslemlub  10536  maxltsup  10547  recn2  10599  imcn2  10600  iiserex  10621  isummolem2a  10662  divalglemnqt  10802  mulgcd  10887  dvdssqlem  10901  nn0seqcvgd  10905  mulgcddvds  10958  rpdvds  10963  pw2dvdseulemle  11027  sqrt2irraplemnn  11039  qden1elz  11065  phimullem  11083  hashgcdlem  11085  hashgcdeq  11086