Theorem breqtrd 4151

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

Syntax hints:   → wi 4   = wceq 1402   class class class wbr 4125

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-br 4126

This theorem is referenced by:  breqtrrd  4153  breqtrid  4162  tfrexlem  6595  phplem4  7146  phplem4on  7159  fidifsnen  7162  fisbth  7177  fin0  7179  fin0or  7180  ltsonq  7755  addlocprlemeqgt  7889  prmuloclemcalc  7922  mullocprlem  7927  addcanprlemu  7972  ltaprlem  7975  ltaprg  7976  prplnqu  7977  ltmprr  7999  cauappcvgprlemopl  8003  cauappcvgprlemloc  8009  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemloc  8032  caucvgprprlemloccalc  8041  caucvgprprlemopl  8054  recexgt0sr  8130  ltm1sr  8134  prsrpos  8142  caucvgsrlemoffgt1  8156  caucvgsr  8159  suplocsrlempr  8164  pitoregt0  8206  axpre-suploclemres  8258  add20  8792  mullt0  8798  ltmul1a  8909  ltm1  9166  recgt0  9170  prodgt0gt0  9171  prodgt0  9172  prodge0  9174  lemul1a  9178  recp1lt1  9219  recreclt  9220  ledivp1  9223  mulle0r  9264  eluzmn  9907  ltaddrp2d  10111  mul2lt0np  10143  xleadd1a  10254  xleaddadd  10268  lincmble  10385  fz01en  10437  fzonmapblen  10577  qbtwnrelemcalc  10668  flqaddz  10710  flhalf  10715  flqdiv  10736  modqmuladdim  10782  modqsubdir  10808  addmodlteq  10813  frecfzen2  10842  iseqf1olemab  10917  ser3le  10952  ltexp2a  11006  leexp2a  11007  exple1  11010  expubnd  11011  bernneq  11076  faclbnd6  11160  hashfz  11240  zfz1isolemiso  11269  zfz1iso  11271  seq3coll  11272  cvg1nlemcxze  11726  cvg1nlemres  11729  recvguniqlem  11738  resqrexlemover  11754  resqrexlemdec  11755  resqrexlemcalc2  11759  resqrexlemcalc3  11760  resqrexlemnm  11762  resqrexlemoverl  11765  ltabs  11831  abslt  11832  absle  11833  abstri  11848  maxabslemlub  11951  maxabslemval  11952  dfabsmax  11961  bdtrilem  11983  xrmaxiflemab  11991  xrmaxiflemlub  11992  xrmaxaddlem  12004  reccn2ap  12057  climge0  12069  climaddc2  12074  summodclem2a  12126  zsumdc  12129  isumge0  12175  fsumle  12208  fsumlt  12209  isumshft  12235  expcnvap0  12247  geolim  12256  geolim2  12257  georeclim  12258  geo2lim  12261  cvgratnnlembern  12268  cvgratnnlemfm  12274  mertenslemi1  12280  mertensabs  12282  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  efcllemp  12403  ef0lem  12405  efgt0  12429  eftlub  12435  efltim  12443  sinbnd  12497  cosbnd  12498  ef01bndlem  12501  sin01gt0  12507  cos01gt0  12508  sin02gt0  12509  eirraplem  12522  dvdssub2  12580  dvdsadd2b  12585  dvdsexp  12606  3dvds  12609  opoe  12640  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  bitsfzolem  12699  bitsinv1lem  12706  gcdaddm  12739  bezoutlemstep  12752  dvdsgcd  12767  dvdsmulgcd  12780  bezoutr1  12788  nninfctlemfo  12795  nn0seqcvgd  12797  rpmulgcd2  12851  qredeq  12852  rpdvds  12855  prmind2  12876  divdenle  12953  phicl2  12970  hashdvds  12977  phimullem  12981  eulerthlemth  12988  prmdiveq  12992  prmdivdiv  12993  pythagtriplem4  13025  pythagtriplem10  13026  pythagtriplem19  13039  pcpre1  13049  pcadd2  13098  qexpz  13109  expnprm  13110  oddprmdvds  13111  pockthlem  13113  4sqlem7  13141  4sqlem10  13144  4sqexercise1  13155  4sqexercise2  13156  4sqlemsdc  13157  4sqlem11  13158  4sqlem12  13159  4sqlem14  13161  4sqlem15  13162  4sqlem16  13163  ennnfonelemkh  13281  ennnfonelemnn0  13291  qusgrp  14012  dvdsrid  14380  dvdsrtr  14381  dvdsrneg  14383  unitmulcl  14393  unitgrp  14396  unitnegcl  14410  subrguss  14517  subrgunit  14520  znidomb  14965  psmetsym  15353  psmettri  15354  mettri2  15386  xmetsym  15392  xmettri  15396  metrtri  15401  xblss2ps  15428  xblss2  15429  blhalf  15432  xmsge0  15491  cnmet  15554  ivthinclemlopn  15660  ivthdichlem  15675  dveflem  15750  dvef  15751  plyaddlem1  15771  sin0pilem1  15805  sinq12gt0  15854  sinq34lt0t  15855  cosq14gt0  15856  coseq0q4123  15858  rpabscxpbnd  15965  logbgcd1irraplemexp  15993  dvdsppwf1o  16017  mpodvdsmulf1o  16018  perfectlem2  16028  lgslem1  16033  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem1  16114  2sqlem3  16150  2sqlem4  16151  2sqlem8  16156  dichmul0orlem1  16667  pwf1oexmid  16943  qdencn  16977  cvgcmp2nlemabs  16986  apdifflemf  17000  apdifflemr  17001