Theorem eqbrtrd 3813

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqbrtrd.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
eqbrtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 3803	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 165	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1285   class class class wbr 3793

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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-br 3794

This theorem is referenced by:  eqbrtrrd  3815  dif1en  6414  prarloclemcalc  6754  ltexprlemopu  6855  recexprlemloc  6883  caucvgprprlemloccalc  6936  mulle0r  8089  lbinfle  8095  divge1  8881  xltnegi  8978  ubmelm1fzo  9312  qbtwnrelemcalc  9342  qbtwnxr  9344  ceiqm1l  9393  ceilqm1lt  9394  ceilqle  9396  modqlt  9415  modqeqmodmin  9476  addmodlteq  9480  bernneq  9690  faclbnd2  9766  resqrexlemdec  10035  resqrexlemcalc2  10039  resqrexlemglsq  10046  resqrexlemga  10047  abslt  10112  amgm2  10142  icodiamlt  10204  maxabsle  10228  maxltsup  10242  minmax  10250  min1inf  10251  min2inf  10252  climconst  10267  iserclim0  10282  mulcn2  10289  iiserex  10315  climlec2  10317  iserige0  10319  climcau  10322  climcvg1nlem  10324  mulgcd  10549  eucalglt  10583  lcmledvds  10596  mulgcddvds  10620  prmind2  10646  pw2dvdslemn  10687  pw2dvdseulemle  10689  oddpwdclemdvds  10692  sqrt2irrap  10702  qdencn  10943