Theorem breqtrd 4015

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

Syntax hints:   → wi 4   = wceq 1348   class class class wbr 3989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990

This theorem is referenced by:  breqtrrd  4017  breqtrid  4026  tfrexlem  6313  phplem4  6833  phplem4on  6845  fidifsnen  6848  fisbth  6861  fin0  6863  fin0or  6864  ltsonq  7360  addlocprlemeqgt  7494  prmuloclemcalc  7527  mullocprlem  7532  addcanprlemu  7577  ltaprlem  7580  ltaprg  7581  prplnqu  7582  ltmprr  7604  cauappcvgprlemopl  7608  cauappcvgprlemloc  7614  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemloc  7637  caucvgprprlemloccalc  7646  caucvgprprlemopl  7659  recexgt0sr  7735  ltm1sr  7739  prsrpos  7747  caucvgsrlemoffgt1  7761  caucvgsr  7764  suplocsrlempr  7769  pitoregt0  7811  axpre-suploclemres  7863  add20  8393  mullt0  8399  ltmul1a  8510  ltm1  8762  recgt0  8766  prodgt0gt0  8767  prodgt0  8768  prodge0  8770  lemul1a  8774  recp1lt1  8815  recreclt  8816  ledivp1  8819  mulle0r  8860  ltaddrp2d  9688  mul2lt0np  9720  xleadd1a  9830  xleaddadd  9844  fz01en  10009  fzonmapblen  10143  qbtwnrelemcalc  10212  flqaddz  10253  flhalf  10258  flqdiv  10277  modqmuladdim  10323  modqsubdir  10349  addmodlteq  10354  frecfzen2  10383  iseqf1olemab  10445  ser3le  10474  ltexp2a  10528  leexp2a  10529  exple1  10532  expubnd  10533  bernneq  10596  faclbnd6  10678  hashfz  10756  zfz1isolemiso  10774  zfz1iso  10776  seq3coll  10777  cvg1nlemcxze  10946  cvg1nlemres  10949  recvguniqlem  10958  resqrexlemover  10974  resqrexlemdec  10975  resqrexlemcalc2  10979  resqrexlemcalc3  10980  resqrexlemnm  10982  resqrexlemoverl  10985  ltabs  11051  abslt  11052  absle  11053  abstri  11068  maxabslemlub  11171  maxabslemval  11172  dfabsmax  11181  bdtrilem  11202  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxaddlem  11223  reccn2ap  11276  climge0  11288  climaddc2  11293  summodclem2a  11344  zsumdc  11347  isumge0  11393  fsumle  11426  fsumlt  11427  isumshft  11453  expcnvap0  11465  geolim  11474  geolim2  11475  georeclim  11476  geo2lim  11479  cvgratnnlembern  11486  cvgratnnlemfm  11492  mertenslemi1  11498  mertensabs  11500  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  efcllemp  11621  ef0lem  11623  efgt0  11647  eftlub  11653  efltim  11661  sinbnd  11715  cosbnd  11716  ef01bndlem  11719  sin01gt0  11724  cos01gt0  11725  sin02gt0  11726  eirraplem  11739  dvdssub2  11797  dvdsadd2b  11802  dvdsexp  11821  opoe  11854  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  gcdaddm  11939  bezoutlemstep  11952  dvdsgcd  11967  dvdsmulgcd  11980  bezoutr1  11988  nn0seqcvgd  11995  rpmulgcd2  12049  qredeq  12050  rpdvds  12053  prmind2  12074  divdenle  12151  phicl2  12168  hashdvds  12175  phimullem  12179  eulerthlemth  12186  prmdiveq  12190  prmdivdiv  12191  pythagtriplem4  12222  pythagtriplem10  12223  pythagtriplem19  12236  pcpre1  12246  qexpz  12304  expnprm  12305  oddprmdvds  12306  pockthlem  12308  4sqlem7  12336  4sqlem10  12339  ennnfonelemkh  12367  ennnfonelemnn0  12377  psmetsym  13123  psmettri  13124  mettri2  13156  xmetsym  13162  xmettri  13166  metrtri  13171  xblss2ps  13198  xblss2  13199  blhalf  13202  xmsge0  13261  cnmet  13324  ivthinclemlopn  13408  dveflem  13481  dvef  13482  sin0pilem1  13496  sinq12gt0  13545  sinq34lt0t  13546  cosq14gt0  13547  coseq0q4123  13549  rpabscxpbnd  13653  logbgcd1irraplemexp  13680  lgslem1  13695  2sqlem3  13747  2sqlem4  13748  2sqlem8  13753  pwf1oexmid  14032  qdencn  14059  cvgcmp2nlemabs  14064  apdifflemf  14078  apdifflemr  14079