Theorem breqtrd 4059

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

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4033

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 3628  df-pr 3629  df-op 3631  df-br 4034

This theorem is referenced by:  breqtrrd  4061  breqtrid  4070  tfrexlem  6392  phplem4  6916  phplem4on  6928  fidifsnen  6931  fisbth  6944  fin0  6946  fin0or  6947  ltsonq  7465  addlocprlemeqgt  7599  prmuloclemcalc  7632  mullocprlem  7637  addcanprlemu  7682  ltaprlem  7685  ltaprg  7686  prplnqu  7687  ltmprr  7709  cauappcvgprlemopl  7713  cauappcvgprlemloc  7719  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemloc  7742  caucvgprprlemloccalc  7751  caucvgprprlemopl  7764  recexgt0sr  7840  ltm1sr  7844  prsrpos  7852  caucvgsrlemoffgt1  7866  caucvgsr  7869  suplocsrlempr  7874  pitoregt0  7916  axpre-suploclemres  7968  add20  8501  mullt0  8507  ltmul1a  8618  ltm1  8873  recgt0  8877  prodgt0gt0  8878  prodgt0  8879  prodge0  8881  lemul1a  8885  recp1lt1  8926  recreclt  8927  ledivp1  8930  mulle0r  8971  ltaddrp2d  9806  mul2lt0np  9838  xleadd1a  9948  xleaddadd  9962  fz01en  10128  fzonmapblen  10263  qbtwnrelemcalc  10345  flqaddz  10387  flhalf  10392  flqdiv  10413  modqmuladdim  10459  modqsubdir  10485  addmodlteq  10490  frecfzen2  10519  iseqf1olemab  10594  ser3le  10629  ltexp2a  10683  leexp2a  10684  exple1  10687  expubnd  10688  bernneq  10752  faclbnd6  10836  hashfz  10913  zfz1isolemiso  10931  zfz1iso  10933  seq3coll  10934  cvg1nlemcxze  11147  cvg1nlemres  11150  recvguniqlem  11159  resqrexlemover  11175  resqrexlemdec  11176  resqrexlemcalc2  11180  resqrexlemcalc3  11181  resqrexlemnm  11183  resqrexlemoverl  11186  ltabs  11252  abslt  11253  absle  11254  abstri  11269  maxabslemlub  11372  maxabslemval  11373  dfabsmax  11382  bdtrilem  11404  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxaddlem  11425  reccn2ap  11478  climge0  11490  climaddc2  11495  summodclem2a  11546  zsumdc  11549  isumge0  11595  fsumle  11628  fsumlt  11629  isumshft  11655  expcnvap0  11667  geolim  11676  geolim2  11677  georeclim  11678  geo2lim  11681  cvgratnnlembern  11688  cvgratnnlemfm  11694  mertenslemi1  11700  mertensabs  11702  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  efcllemp  11823  ef0lem  11825  efgt0  11849  eftlub  11855  efltim  11863  sinbnd  11917  cosbnd  11918  ef01bndlem  11921  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  eirraplem  11942  dvdssub2  12000  dvdsadd2b  12005  dvdsexp  12026  3dvds  12029  opoe  12060  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  bitsfzolem  12118  gcdaddm  12151  bezoutlemstep  12164  dvdsgcd  12179  dvdsmulgcd  12192  bezoutr1  12200  nninfctlemfo  12207  nn0seqcvgd  12209  rpmulgcd2  12263  qredeq  12264  rpdvds  12267  prmind2  12288  divdenle  12365  phicl2  12382  hashdvds  12389  phimullem  12393  eulerthlemth  12400  prmdiveq  12404  prmdivdiv  12405  pythagtriplem4  12437  pythagtriplem10  12438  pythagtriplem19  12451  pcpre1  12461  pcadd2  12510  qexpz  12521  expnprm  12522  oddprmdvds  12523  pockthlem  12525  4sqlem7  12553  4sqlem10  12556  4sqexercise1  12567  4sqexercise2  12568  4sqlemsdc  12569  4sqlem11  12570  4sqlem12  12571  4sqlem14  12573  4sqlem15  12574  4sqlem16  12575  ennnfonelemkh  12629  ennnfonelemnn0  12639  qusgrp  13362  dvdsrid  13656  dvdsrtr  13657  dvdsrneg  13659  unitmulcl  13669  unitgrp  13672  unitnegcl  13686  subrguss  13792  subrgunit  13795  znidomb  14214  psmetsym  14565  psmettri  14566  mettri2  14598  xmetsym  14604  xmettri  14608  metrtri  14613  xblss2ps  14640  xblss2  14641  blhalf  14644  xmsge0  14703  cnmet  14766  ivthinclemlopn  14872  ivthdichlem  14887  dveflem  14962  dvef  14963  plyaddlem1  14983  sin0pilem1  15017  sinq12gt0  15066  sinq34lt0t  15067  cosq14gt0  15068  coseq0q4123  15070  rpabscxpbnd  15176  logbgcd1irraplemexp  15204  dvdsppwf1o  15225  mpodvdsmulf1o  15226  perfectlem2  15236  lgslem1  15241  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem1  15322  2sqlem3  15358  2sqlem4  15359  2sqlem8  15364  pwf1oexmid  15644  qdencn  15671  cvgcmp2nlemabs  15676  apdifflemf  15690  apdifflemr  15691