Theorem eqbrtrd 4055

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

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4033

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034

This theorem is referenced by:  eqbrtrrd  4057  dif1en  6940  ccfunen  7331  prarloclemcalc  7569  ltexprlemopu  7670  recexprlemloc  7698  caucvgprprlemloccalc  7751  suplocsrlem  7875  axpre-suploclemres  7968  mulle0r  8971  lbinfle  8977  divge1  9798  xltnegi  9910  xleadd1a  9948  xltadd1  9951  xlt2add  9955  xposdif  9957  xleaddadd  9962  ubmelm1fzo  10302  zsupssdc  10328  qbtwnrelemcalc  10345  qbtwnxr  10347  ceiqm1l  10403  ceilqm1lt  10404  ceilqle  10406  modqlt  10425  modqeqmodmin  10486  addmodlteq  10490  seqf1oglem1  10611  exp3vallem  10632  bernneq  10752  nn0ltexp2  10801  faclbnd2  10834  resqrexlemdec  11176  resqrexlemcalc2  11180  resqrexlemglsq  11187  resqrexlemga  11188  abslt  11253  amgm2  11283  icodiamlt  11345  maxabsle  11369  maxltsup  11383  minmax  11395  min1inf  11397  min2inf  11398  bdtrilem  11404  xrmaxltsup  11423  xrmaxaddlem  11425  xrmaxadd  11426  xrminmax  11430  xrmin1inf  11432  xrmin2inf  11433  climconst  11455  serclim0  11470  mulcn2  11477  reccn2ap  11478  iserex  11504  climlec2  11506  iserge0  11508  climcau  11512  climcvg1nlem  11514  fsumabs  11630  iserabs  11640  isumlessdc  11661  divcnv  11662  expcnvre  11668  absgtap  11675  georeclim  11678  cvgratnnlembern  11688  cvgratnnlemsumlt  11693  cvgratnnlemfm  11694  cvgratnnlemrate  11695  mertenslemub  11699  mertenslemi1  11700  prodfclim1  11709  prodfap0  11710  efcvgfsum  11832  eftlub  11855  eflegeo  11866  tanval3ap  11879  tannegap  11893  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  cos01gt0  11928  bitsfzolem  12118  bitsfzo  12119  mulgcd  12183  nnminle  12202  eucalglt  12225  lcmledvds  12238  mulgcddvds  12262  prmind2  12288  isprm5lem  12309  pw2dvdslemn  12333  pw2dvdseulemle  12335  oddpwdclemdvds  12338  sqrt2irrap  12348  divdenle  12365  nonsq  12375  pythagtriplem4  12437  pclem0  12455  pcpremul  12462  pczdvds  12483  pcprmpw2  12502  qexpz  12521  4sqlem10  12556  ennnfonelemkh  12629  triv1nsgd  13348  qusgrp  13362  bl2in  14639  xblcntrps  14649  xblcntr  14650  ssblps  14661  ssbl  14662  blssps  14663  blss  14664  xmetxp  14743  mulc1cncf  14825  cncfmptc  14832  mulcncflem  14843  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthdec  14880  ivthreinc  14881  hovera  14883  hoverlt1  14885  limcimolemlt  14900  cnplimclemle  14904  cnplimclemr  14905  limccnp2lem  14912  dveflem  14962  reeff1olem  15007  reeff1oleme  15008  tangtx  15074  cosq34lt1  15086  logdivlti  15117  cxpap0  15140  rpabscxpbnd  15176  mersenne  15233  lgslem3  15243  gausslemma2dlem1a  15299  lgsquadlem1  15318  lgsquadlem2  15319  2lgslem1c  15331  qdencn  15671  cvgcmp2nlemabs  15676  trilpolemclim  15680  trilpolemisumle  15682  trilpolemeq1  15684  apdifflemf  15690  apdifflemr  15691