Theorem eqbrtrd 4076

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 4064	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 167	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4054

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-br 4055

This theorem is referenced by:  eqbrtrrd  4078  dif1en  6997  ccfunen  7406  prarloclemcalc  7645  ltexprlemopu  7746  recexprlemloc  7774  caucvgprprlemloccalc  7827  suplocsrlem  7951  axpre-suploclemres  8044  mulle0r  9047  lbinfle  9053  divge1  9875  xltnegi  9987  xleadd1a  10025  xltadd1  10028  xlt2add  10032  xposdif  10034  xleaddadd  10039  ubmelm1fzo  10387  zsupssdc  10413  qbtwnrelemcalc  10430  qbtwnxr  10432  ceiqm1l  10488  ceilqm1lt  10489  ceilqle  10491  modqlt  10510  modqeqmodmin  10571  addmodlteq  10575  seqf1oglem1  10696  exp3vallem  10717  bernneq  10837  nn0ltexp2  10886  faclbnd2  10919  ccatsymb  11091  ccatrn  11098  resqrexlemdec  11407  resqrexlemcalc2  11411  resqrexlemglsq  11418  resqrexlemga  11419  abslt  11484  amgm2  11514  icodiamlt  11576  maxabsle  11600  maxltsup  11614  minmax  11626  min1inf  11628  min2inf  11629  bdtrilem  11635  xrmaxltsup  11654  xrmaxaddlem  11656  xrmaxadd  11657  xrminmax  11661  xrmin1inf  11663  xrmin2inf  11664  climconst  11686  serclim0  11701  mulcn2  11708  reccn2ap  11709  iserex  11735  climlec2  11737  iserge0  11739  climcau  11743  climcvg1nlem  11745  fsumabs  11861  iserabs  11871  isumlessdc  11892  divcnv  11893  expcnvre  11899  absgtap  11906  georeclim  11909  cvgratnnlembern  11919  cvgratnnlemsumlt  11924  cvgratnnlemfm  11925  cvgratnnlemrate  11926  mertenslemub  11930  mertenslemi1  11931  prodfclim1  11940  prodfap0  11941  efcvgfsum  12063  eftlub  12086  eflegeo  12097  tanval3ap  12110  tannegap  12124  ef01bndlem  12152  sin01bnd  12153  cos01bnd  12154  cos01gt0  12159  bitsfzolem  12350  bitsfzo  12351  bitsinv1lem  12357  mulgcd  12422  nnminle  12441  eucalglt  12464  lcmledvds  12477  mulgcddvds  12501  prmind2  12527  isprm5lem  12548  pw2dvdslemn  12572  pw2dvdseulemle  12574  oddpwdclemdvds  12577  sqrt2irrap  12587  divdenle  12604  nonsq  12614  pythagtriplem4  12676  pclem0  12694  pcpremul  12701  pczdvds  12722  pcprmpw2  12741  qexpz  12760  4sqlem10  12795  ennnfonelemkh  12868  prdsbaslemss  13191  triv1nsgd  13639  qusgrp  13653  bl2in  14960  xblcntrps  14970  xblcntr  14971  ssblps  14982  ssbl  14983  blssps  14984  blss  14985  xmetxp  15064  mulc1cncf  15146  cncfmptc  15153  mulcncflem  15164  ivthinclemlopn  15193  ivthinclemuopn  15195  ivthdec  15201  ivthreinc  15202  hovera  15204  hoverlt1  15206  limcimolemlt  15221  cnplimclemle  15225  cnplimclemr  15226  limccnp2lem  15233  dveflem  15283  reeff1olem  15328  reeff1oleme  15329  tangtx  15395  cosq34lt1  15407  logdivlti  15438  cxpap0  15461  rpabscxpbnd  15497  mersenne  15554  lgslem3  15564  gausslemma2dlem1a  15620  lgsquadlem1  15639  lgsquadlem2  15640  2lgslem1c  15652  qdencn  16138  cvgcmp2nlemabs  16143  trilpolemclim  16147  trilpolemisumle  16149  trilpolemeq1  16151  apdifflemf  16157  apdifflemr  16158