Theorem eqbrtrd 4108

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

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4086

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  eqbrtrrd  4110  dif1en  7061  ccfunen  7473  prarloclemcalc  7712  ltexprlemopu  7813  recexprlemloc  7841  caucvgprprlemloccalc  7894  suplocsrlem  8018  axpre-suploclemres  8111  mulle0r  9114  lbinfle  9120  divge1  9948  xltnegi  10060  xleadd1a  10098  xltadd1  10101  xlt2add  10105  xposdif  10107  xleaddadd  10112  ubmelm1fzo  10461  zsupssdc  10488  qbtwnrelemcalc  10505  qbtwnxr  10507  ceiqm1l  10563  ceilqm1lt  10564  ceilqle  10566  modqlt  10585  modqeqmodmin  10646  addmodlteq  10650  seqf1oglem1  10771  exp3vallem  10792  bernneq  10912  nn0ltexp2  10961  faclbnd2  10994  ccatsymb  11169  ccatrn  11176  resqrexlemdec  11562  resqrexlemcalc2  11566  resqrexlemglsq  11573  resqrexlemga  11574  abslt  11639  amgm2  11669  icodiamlt  11731  maxabsle  11755  maxltsup  11769  minmax  11781  min1inf  11783  min2inf  11784  bdtrilem  11790  xrmaxltsup  11809  xrmaxaddlem  11811  xrmaxadd  11812  xrminmax  11816  xrmin1inf  11818  xrmin2inf  11819  climconst  11841  serclim0  11856  mulcn2  11863  reccn2ap  11864  iserex  11890  climlec2  11892  iserge0  11894  climcau  11898  climcvg1nlem  11900  fsumabs  12016  iserabs  12026  isumlessdc  12047  divcnv  12048  expcnvre  12054  absgtap  12061  georeclim  12064  cvgratnnlembern  12074  cvgratnnlemsumlt  12079  cvgratnnlemfm  12080  cvgratnnlemrate  12081  mertenslemub  12085  mertenslemi1  12086  prodfclim1  12095  prodfap0  12096  efcvgfsum  12218  eftlub  12241  eflegeo  12252  tanval3ap  12265  tannegap  12279  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  cos01gt0  12314  bitsfzolem  12505  bitsfzo  12506  bitsinv1lem  12512  mulgcd  12577  nnminle  12596  eucalglt  12619  lcmledvds  12632  mulgcddvds  12656  prmind2  12682  isprm5lem  12703  pw2dvdslemn  12727  pw2dvdseulemle  12729  oddpwdclemdvds  12732  sqrt2irrap  12742  divdenle  12759  nonsq  12769  pythagtriplem4  12831  pclem0  12849  pcpremul  12856  pczdvds  12877  pcprmpw2  12896  qexpz  12915  4sqlem10  12950  ennnfonelemkh  13023  prdsbaslemss  13347  triv1nsgd  13795  qusgrp  13809  bl2in  15117  xblcntrps  15127  xblcntr  15128  ssblps  15139  ssbl  15140  blssps  15141  blss  15142  xmetxp  15221  mulc1cncf  15303  cncfmptc  15310  mulcncflem  15321  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthdec  15358  ivthreinc  15359  hovera  15361  hoverlt1  15363  limcimolemlt  15378  cnplimclemle  15382  cnplimclemr  15383  limccnp2lem  15390  dveflem  15440  reeff1olem  15485  reeff1oleme  15486  tangtx  15552  cosq34lt1  15564  logdivlti  15595  cxpap0  15618  rpabscxpbnd  15654  mersenne  15711  lgslem3  15721  gausslemma2dlem1a  15777  lgsquadlem1  15796  lgsquadlem2  15797  2lgslem1c  15809  qdencn  16567  cvgcmp2nlemabs  16572  trilpolemclim  16576  trilpolemisumle  16578  trilpolemeq1  16580  apdifflemf  16586  apdifflemr  16587