Theorem eqbrtrd 4056

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

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

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 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  eqbrtrrd  4058  dif1en  6949  ccfunen  7349  prarloclemcalc  7588  ltexprlemopu  7689  recexprlemloc  7717  caucvgprprlemloccalc  7770  suplocsrlem  7894  axpre-suploclemres  7987  mulle0r  8990  lbinfle  8996  divge1  9817  xltnegi  9929  xleadd1a  9967  xltadd1  9970  xlt2add  9974  xposdif  9976  xleaddadd  9981  ubmelm1fzo  10321  zsupssdc  10347  qbtwnrelemcalc  10364  qbtwnxr  10366  ceiqm1l  10422  ceilqm1lt  10423  ceilqle  10425  modqlt  10444  modqeqmodmin  10505  addmodlteq  10509  seqf1oglem1  10630  exp3vallem  10651  bernneq  10771  nn0ltexp2  10820  faclbnd2  10853  resqrexlemdec  11195  resqrexlemcalc2  11199  resqrexlemglsq  11206  resqrexlemga  11207  abslt  11272  amgm2  11302  icodiamlt  11364  maxabsle  11388  maxltsup  11402  minmax  11414  min1inf  11416  min2inf  11417  bdtrilem  11423  xrmaxltsup  11442  xrmaxaddlem  11444  xrmaxadd  11445  xrminmax  11449  xrmin1inf  11451  xrmin2inf  11452  climconst  11474  serclim0  11489  mulcn2  11496  reccn2ap  11497  iserex  11523  climlec2  11525  iserge0  11527  climcau  11531  climcvg1nlem  11533  fsumabs  11649  iserabs  11659  isumlessdc  11680  divcnv  11681  expcnvre  11687  absgtap  11694  georeclim  11697  cvgratnnlembern  11707  cvgratnnlemsumlt  11712  cvgratnnlemfm  11713  cvgratnnlemrate  11714  mertenslemub  11718  mertenslemi1  11719  prodfclim1  11728  prodfap0  11729  efcvgfsum  11851  eftlub  11874  eflegeo  11885  tanval3ap  11898  tannegap  11912  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  cos01gt0  11947  bitsfzolem  12138  bitsfzo  12139  bitsinv1lem  12145  mulgcd  12210  nnminle  12229  eucalglt  12252  lcmledvds  12265  mulgcddvds  12289  prmind2  12315  isprm5lem  12336  pw2dvdslemn  12360  pw2dvdseulemle  12362  oddpwdclemdvds  12365  sqrt2irrap  12375  divdenle  12392  nonsq  12402  pythagtriplem4  12464  pclem0  12482  pcpremul  12489  pczdvds  12510  pcprmpw2  12529  qexpz  12548  4sqlem10  12583  ennnfonelemkh  12656  prdsbaslemss  12978  triv1nsgd  13426  qusgrp  13440  bl2in  14747  xblcntrps  14757  xblcntr  14758  ssblps  14769  ssbl  14770  blssps  14771  blss  14772  xmetxp  14851  mulc1cncf  14933  cncfmptc  14940  mulcncflem  14951  ivthinclemlopn  14980  ivthinclemuopn  14982  ivthdec  14988  ivthreinc  14989  hovera  14991  hoverlt1  14993  limcimolemlt  15008  cnplimclemle  15012  cnplimclemr  15013  limccnp2lem  15020  dveflem  15070  reeff1olem  15115  reeff1oleme  15116  tangtx  15182  cosq34lt1  15194  logdivlti  15225  cxpap0  15248  rpabscxpbnd  15284  mersenne  15341  lgslem3  15351  gausslemma2dlem1a  15407  lgsquadlem1  15426  lgsquadlem2  15427  2lgslem1c  15439  qdencn  15784  cvgcmp2nlemabs  15789  trilpolemclim  15793  trilpolemisumle  15795  trilpolemeq1  15797  apdifflemf  15803  apdifflemr  15804