Theorem breqtrd 4055

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  breqtrrd  4057  breqtrid  4066  tfrexlem  6387  phplem4  6911  phplem4on  6923  fidifsnen  6926  fisbth  6939  fin0  6941  fin0or  6942  ltsonq  7458  addlocprlemeqgt  7592  prmuloclemcalc  7625  mullocprlem  7630  addcanprlemu  7675  ltaprlem  7678  ltaprg  7679  prplnqu  7680  ltmprr  7702  cauappcvgprlemopl  7706  cauappcvgprlemloc  7712  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemloc  7735  caucvgprprlemloccalc  7744  caucvgprprlemopl  7757  recexgt0sr  7833  ltm1sr  7837  prsrpos  7845  caucvgsrlemoffgt1  7859  caucvgsr  7862  suplocsrlempr  7867  pitoregt0  7909  axpre-suploclemres  7961  add20  8493  mullt0  8499  ltmul1a  8610  ltm1  8865  recgt0  8869  prodgt0gt0  8870  prodgt0  8871  prodge0  8873  lemul1a  8877  recp1lt1  8918  recreclt  8919  ledivp1  8922  mulle0r  8963  ltaddrp2d  9797  mul2lt0np  9829  xleadd1a  9939  xleaddadd  9953  fz01en  10119  fzonmapblen  10254  qbtwnrelemcalc  10324  flqaddz  10366  flhalf  10371  flqdiv  10392  modqmuladdim  10438  modqsubdir  10464  addmodlteq  10469  frecfzen2  10498  iseqf1olemab  10573  ser3le  10608  ltexp2a  10662  leexp2a  10663  exple1  10666  expubnd  10667  bernneq  10731  faclbnd6  10815  hashfz  10892  zfz1isolemiso  10910  zfz1iso  10912  seq3coll  10913  cvg1nlemcxze  11126  cvg1nlemres  11129  recvguniqlem  11138  resqrexlemover  11154  resqrexlemdec  11155  resqrexlemcalc2  11159  resqrexlemcalc3  11160  resqrexlemnm  11162  resqrexlemoverl  11165  ltabs  11231  abslt  11232  absle  11233  abstri  11248  maxabslemlub  11351  maxabslemval  11352  dfabsmax  11361  bdtrilem  11382  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxaddlem  11403  reccn2ap  11456  climge0  11468  climaddc2  11473  summodclem2a  11524  zsumdc  11527  isumge0  11573  fsumle  11606  fsumlt  11607  isumshft  11633  expcnvap0  11645  geolim  11654  geolim2  11655  georeclim  11656  geo2lim  11659  cvgratnnlembern  11666  cvgratnnlemfm  11672  mertenslemi1  11678  mertensabs  11680  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  efcllemp  11801  ef0lem  11803  efgt0  11827  eftlub  11833  efltim  11841  sinbnd  11895  cosbnd  11896  ef01bndlem  11899  sin01gt0  11905  cos01gt0  11906  sin02gt0  11907  eirraplem  11920  dvdssub2  11978  dvdsadd2b  11983  dvdsexp  12003  opoe  12036  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  gcdaddm  12121  bezoutlemstep  12134  dvdsgcd  12149  dvdsmulgcd  12162  bezoutr1  12170  nninfctlemfo  12177  nn0seqcvgd  12179  rpmulgcd2  12233  qredeq  12234  rpdvds  12237  prmind2  12258  divdenle  12335  phicl2  12352  hashdvds  12359  phimullem  12363  eulerthlemth  12370  prmdiveq  12374  prmdivdiv  12375  pythagtriplem4  12406  pythagtriplem10  12407  pythagtriplem19  12420  pcpre1  12430  pcadd2  12479  qexpz  12490  expnprm  12491  oddprmdvds  12492  pockthlem  12494  4sqlem7  12522  4sqlem10  12525  4sqexercise1  12536  4sqexercise2  12537  4sqlemsdc  12538  4sqlem11  12539  4sqlem12  12540  4sqlem14  12542  4sqlem15  12543  4sqlem16  12544  ennnfonelemkh  12569  ennnfonelemnn0  12579  qusgrp  13302  dvdsrid  13596  dvdsrtr  13597  dvdsrneg  13599  unitmulcl  13609  unitgrp  13612  unitnegcl  13626  subrguss  13732  subrgunit  13735  znidomb  14146  psmetsym  14497  psmettri  14498  mettri2  14530  xmetsym  14536  xmettri  14540  metrtri  14545  xblss2ps  14572  xblss2  14573  blhalf  14576  xmsge0  14635  cnmet  14698  ivthinclemlopn  14790  ivthdichlem  14805  dveflem  14872  dvef  14873  plyaddlem1  14893  sin0pilem1  14916  sinq12gt0  14965  sinq34lt0t  14966  cosq14gt0  14967  coseq0q4123  14969  rpabscxpbnd  15073  logbgcd1irraplemexp  15100  lgslem1  15116  lgseisenlem2  15187  lgsquadlem1  15191  2sqlem3  15204  2sqlem4  15205  2sqlem8  15210  pwf1oexmid  15490  qdencn  15517  cvgcmp2nlemabs  15522  apdifflemf  15536  apdifflemr  15537