Theorem breqtrd 4112

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

Hypotheses

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

Assertion

Ref	Expression
breqtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrd

Step	Hyp	Ref	Expression
1		breqtrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	breq2d 4098	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 147	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:  breqtrrd  4114  breqtrid  4123  tfrexlem  6495  phplem4  7036  phplem4on  7049  fidifsnen  7052  fisbth  7065  fin0  7067  fin0or  7068  ltsonq  7608  addlocprlemeqgt  7742  prmuloclemcalc  7775  mullocprlem  7780  addcanprlemu  7825  ltaprlem  7828  ltaprg  7829  prplnqu  7830  ltmprr  7852  cauappcvgprlemopl  7856  cauappcvgprlemloc  7862  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemloc  7885  caucvgprprlemloccalc  7894  caucvgprprlemopl  7907  recexgt0sr  7983  ltm1sr  7987  prsrpos  7995  caucvgsrlemoffgt1  8009  caucvgsr  8012  suplocsrlempr  8017  pitoregt0  8059  axpre-suploclemres  8111  add20  8644  mullt0  8650  ltmul1a  8761  ltm1  9016  recgt0  9020  prodgt0gt0  9021  prodgt0  9022  prodge0  9024  lemul1a  9028  recp1lt1  9069  recreclt  9070  ledivp1  9073  mulle0r  9114  eluzmn  9752  ltaddrp2d  9956  mul2lt0np  9988  xleadd1a  10098  xleaddadd  10112  fz01en  10278  fzonmapblen  10416  qbtwnrelemcalc  10505  flqaddz  10547  flhalf  10552  flqdiv  10573  modqmuladdim  10619  modqsubdir  10645  addmodlteq  10650  frecfzen2  10679  iseqf1olemab  10754  ser3le  10789  ltexp2a  10843  leexp2a  10844  exple1  10847  expubnd  10848  bernneq  10912  faclbnd6  10996  hashfz  11075  zfz1isolemiso  11093  zfz1iso  11095  seq3coll  11096  cvg1nlemcxze  11533  cvg1nlemres  11536  recvguniqlem  11545  resqrexlemover  11561  resqrexlemdec  11562  resqrexlemcalc2  11566  resqrexlemcalc3  11567  resqrexlemnm  11569  resqrexlemoverl  11572  ltabs  11638  abslt  11639  absle  11640  abstri  11655  maxabslemlub  11758  maxabslemval  11759  dfabsmax  11768  bdtrilem  11790  xrmaxiflemab  11798  xrmaxiflemlub  11799  xrmaxaddlem  11811  reccn2ap  11864  climge0  11876  climaddc2  11881  summodclem2a  11932  zsumdc  11935  isumge0  11981  fsumle  12014  fsumlt  12015  isumshft  12041  expcnvap0  12053  geolim  12062  geolim2  12063  georeclim  12064  geo2lim  12067  cvgratnnlembern  12074  cvgratnnlemfm  12080  mertenslemi1  12086  mertensabs  12088  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  efcllemp  12209  ef0lem  12211  efgt0  12235  eftlub  12241  efltim  12249  sinbnd  12303  cosbnd  12304  ef01bndlem  12307  sin01gt0  12313  cos01gt0  12314  sin02gt0  12315  eirraplem  12328  dvdssub2  12386  dvdsadd2b  12391  dvdsexp  12412  3dvds  12415  opoe  12446  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  bitsfzolem  12505  bitsinv1lem  12512  gcdaddm  12545  bezoutlemstep  12558  dvdsgcd  12573  dvdsmulgcd  12586  bezoutr1  12594  nninfctlemfo  12601  nn0seqcvgd  12603  rpmulgcd2  12657  qredeq  12658  rpdvds  12661  prmind2  12682  divdenle  12759  phicl2  12776  hashdvds  12783  phimullem  12787  eulerthlemth  12794  prmdiveq  12798  prmdivdiv  12799  pythagtriplem4  12831  pythagtriplem10  12832  pythagtriplem19  12845  pcpre1  12855  pcadd2  12904  qexpz  12915  expnprm  12916  oddprmdvds  12917  pockthlem  12919  4sqlem7  12947  4sqlem10  12950  4sqexercise1  12961  4sqexercise2  12962  4sqlemsdc  12963  4sqlem11  12964  4sqlem12  12965  4sqlem14  12967  4sqlem15  12968  4sqlem16  12969  ennnfonelemkh  13023  ennnfonelemnn0  13033  qusgrp  13809  dvdsrid  14104  dvdsrtr  14105  dvdsrneg  14107  unitmulcl  14117  unitgrp  14120  unitnegcl  14134  subrguss  14240  subrgunit  14243  znidomb  14662  psmetsym  15043  psmettri  15044  mettri2  15076  xmetsym  15082  xmettri  15086  metrtri  15091  xblss2ps  15118  xblss2  15119  blhalf  15122  xmsge0  15181  cnmet  15244  ivthinclemlopn  15350  ivthdichlem  15365  dveflem  15440  dvef  15441  plyaddlem1  15461  sin0pilem1  15495  sinq12gt0  15544  sinq34lt0t  15545  cosq14gt0  15546  coseq0q4123  15548  rpabscxpbnd  15654  logbgcd1irraplemexp  15682  dvdsppwf1o  15703  mpodvdsmulf1o  15704  perfectlem2  15714  lgslem1  15719  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem1  15800  2sqlem3  15836  2sqlem4  15837  2sqlem8  15842  pwf1oexmid  16536  qdencn  16567  cvgcmp2nlemabs  16572  apdifflemf  16586  apdifflemr  16587