Theorem breqtrd 4060

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 4046	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 147	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:  breqtrrd  4062  breqtrid  4071  tfrexlem  6401  phplem4  6925  phplem4on  6937  fidifsnen  6940  fisbth  6953  fin0  6955  fin0or  6956  ltsonq  7482  addlocprlemeqgt  7616  prmuloclemcalc  7649  mullocprlem  7654  addcanprlemu  7699  ltaprlem  7702  ltaprg  7703  prplnqu  7704  ltmprr  7726  cauappcvgprlemopl  7730  cauappcvgprlemloc  7736  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemloc  7759  caucvgprprlemloccalc  7768  caucvgprprlemopl  7781  recexgt0sr  7857  ltm1sr  7861  prsrpos  7869  caucvgsrlemoffgt1  7883  caucvgsr  7886  suplocsrlempr  7891  pitoregt0  7933  axpre-suploclemres  7985  add20  8518  mullt0  8524  ltmul1a  8635  ltm1  8890  recgt0  8894  prodgt0gt0  8895  prodgt0  8896  prodge0  8898  lemul1a  8902  recp1lt1  8943  recreclt  8944  ledivp1  8947  mulle0r  8988  ltaddrp2d  9823  mul2lt0np  9855  xleadd1a  9965  xleaddadd  9979  fz01en  10145  fzonmapblen  10280  qbtwnrelemcalc  10362  flqaddz  10404  flhalf  10409  flqdiv  10430  modqmuladdim  10476  modqsubdir  10502  addmodlteq  10507  frecfzen2  10536  iseqf1olemab  10611  ser3le  10646  ltexp2a  10700  leexp2a  10701  exple1  10704  expubnd  10705  bernneq  10769  faclbnd6  10853  hashfz  10930  zfz1isolemiso  10948  zfz1iso  10950  seq3coll  10951  cvg1nlemcxze  11164  cvg1nlemres  11167  recvguniqlem  11176  resqrexlemover  11192  resqrexlemdec  11193  resqrexlemcalc2  11197  resqrexlemcalc3  11198  resqrexlemnm  11200  resqrexlemoverl  11203  ltabs  11269  abslt  11270  absle  11271  abstri  11286  maxabslemlub  11389  maxabslemval  11390  dfabsmax  11399  bdtrilem  11421  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxaddlem  11442  reccn2ap  11495  climge0  11507  climaddc2  11512  summodclem2a  11563  zsumdc  11566  isumge0  11612  fsumle  11645  fsumlt  11646  isumshft  11672  expcnvap0  11684  geolim  11693  geolim2  11694  georeclim  11695  geo2lim  11698  cvgratnnlembern  11705  cvgratnnlemfm  11711  mertenslemi1  11717  mertensabs  11719  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  efcllemp  11840  ef0lem  11842  efgt0  11866  eftlub  11872  efltim  11880  sinbnd  11934  cosbnd  11935  ef01bndlem  11938  sin01gt0  11944  cos01gt0  11945  sin02gt0  11946  eirraplem  11959  dvdssub2  12017  dvdsadd2b  12022  dvdsexp  12043  3dvds  12046  opoe  12077  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  bitsfzolem  12136  bitsinv1lem  12143  gcdaddm  12176  bezoutlemstep  12189  dvdsgcd  12204  dvdsmulgcd  12217  bezoutr1  12225  nninfctlemfo  12232  nn0seqcvgd  12234  rpmulgcd2  12288  qredeq  12289  rpdvds  12292  prmind2  12313  divdenle  12390  phicl2  12407  hashdvds  12414  phimullem  12418  eulerthlemth  12425  prmdiveq  12429  prmdivdiv  12430  pythagtriplem4  12462  pythagtriplem10  12463  pythagtriplem19  12476  pcpre1  12486  pcadd2  12535  qexpz  12546  expnprm  12547  oddprmdvds  12548  pockthlem  12550  4sqlem7  12578  4sqlem10  12581  4sqexercise1  12592  4sqexercise2  12593  4sqlemsdc  12594  4sqlem11  12595  4sqlem12  12596  4sqlem14  12598  4sqlem15  12599  4sqlem16  12600  ennnfonelemkh  12654  ennnfonelemnn0  12664  qusgrp  13438  dvdsrid  13732  dvdsrtr  13733  dvdsrneg  13735  unitmulcl  13745  unitgrp  13748  unitnegcl  13762  subrguss  13868  subrgunit  13871  znidomb  14290  psmetsym  14649  psmettri  14650  mettri2  14682  xmetsym  14688  xmettri  14692  metrtri  14697  xblss2ps  14724  xblss2  14725  blhalf  14728  xmsge0  14787  cnmet  14850  ivthinclemlopn  14956  ivthdichlem  14971  dveflem  15046  dvef  15047  plyaddlem1  15067  sin0pilem1  15101  sinq12gt0  15150  sinq34lt0t  15151  cosq14gt0  15152  coseq0q4123  15154  rpabscxpbnd  15260  logbgcd1irraplemexp  15288  dvdsppwf1o  15309  mpodvdsmulf1o  15310  perfectlem2  15320  lgslem1  15325  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem1  15406  2sqlem3  15442  2sqlem4  15443  2sqlem8  15448  pwf1oexmid  15730  qdencn  15758  cvgcmp2nlemabs  15763  apdifflemf  15777  apdifflemr  15778