Theorem breqtrd 4029

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

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 4003

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004

This theorem is referenced by:  breqtrrd  4031  breqtrid  4040  tfrexlem  6334  phplem4  6854  phplem4on  6866  fidifsnen  6869  fisbth  6882  fin0  6884  fin0or  6885  ltsonq  7396  addlocprlemeqgt  7530  prmuloclemcalc  7563  mullocprlem  7568  addcanprlemu  7613  ltaprlem  7616  ltaprg  7617  prplnqu  7618  ltmprr  7640  cauappcvgprlemopl  7644  cauappcvgprlemloc  7650  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem1  7657  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemloc  7673  caucvgprprlemloccalc  7682  caucvgprprlemopl  7695  recexgt0sr  7771  ltm1sr  7775  prsrpos  7783  caucvgsrlemoffgt1  7797  caucvgsr  7800  suplocsrlempr  7805  pitoregt0  7847  axpre-suploclemres  7899  add20  8430  mullt0  8436  ltmul1a  8547  ltm1  8802  recgt0  8806  prodgt0gt0  8807  prodgt0  8808  prodge0  8810  lemul1a  8814  recp1lt1  8855  recreclt  8856  ledivp1  8859  mulle0r  8900  ltaddrp2d  9730  mul2lt0np  9762  xleadd1a  9872  xleaddadd  9886  fz01en  10052  fzonmapblen  10186  qbtwnrelemcalc  10255  flqaddz  10296  flhalf  10301  flqdiv  10320  modqmuladdim  10366  modqsubdir  10392  addmodlteq  10397  frecfzen2  10426  iseqf1olemab  10488  ser3le  10517  ltexp2a  10571  leexp2a  10572  exple1  10575  expubnd  10576  bernneq  10640  faclbnd6  10723  hashfz  10800  zfz1isolemiso  10818  zfz1iso  10820  seq3coll  10821  cvg1nlemcxze  10990  cvg1nlemres  10993  recvguniqlem  11002  resqrexlemover  11018  resqrexlemdec  11019  resqrexlemcalc2  11023  resqrexlemcalc3  11024  resqrexlemnm  11026  resqrexlemoverl  11029  ltabs  11095  abslt  11096  absle  11097  abstri  11112  maxabslemlub  11215  maxabslemval  11216  dfabsmax  11225  bdtrilem  11246  xrmaxiflemab  11254  xrmaxiflemlub  11255  xrmaxaddlem  11267  reccn2ap  11320  climge0  11332  climaddc2  11337  summodclem2a  11388  zsumdc  11391  isumge0  11437  fsumle  11470  fsumlt  11471  isumshft  11497  expcnvap0  11509  geolim  11518  geolim2  11519  georeclim  11520  geo2lim  11523  cvgratnnlembern  11530  cvgratnnlemfm  11536  mertenslemi1  11542  mertensabs  11544  prodmodclem3  11582  prodmodclem2a  11583  zproddc  11586  fprodseq  11590  efcllemp  11665  ef0lem  11667  efgt0  11691  eftlub  11697  efltim  11705  sinbnd  11759  cosbnd  11760  ef01bndlem  11763  sin01gt0  11768  cos01gt0  11769  sin02gt0  11770  eirraplem  11783  dvdssub2  11841  dvdsadd2b  11846  dvdsexp  11866  opoe  11899  divalglemeunn  11925  divalglemex  11926  divalglemeuneg  11927  gcdaddm  11984  bezoutlemstep  11997  dvdsgcd  12012  dvdsmulgcd  12025  bezoutr1  12033  nn0seqcvgd  12040  rpmulgcd2  12094  qredeq  12095  rpdvds  12098  prmind2  12119  divdenle  12196  phicl2  12213  hashdvds  12220  phimullem  12224  eulerthlemth  12231  prmdiveq  12235  prmdivdiv  12236  pythagtriplem4  12267  pythagtriplem10  12268  pythagtriplem19  12281  pcpre1  12291  qexpz  12349  expnprm  12350  oddprmdvds  12351  pockthlem  12353  4sqlem7  12381  4sqlem10  12384  ennnfonelemkh  12412  ennnfonelemnn0  12422  dvdsrid  13267  dvdsrtr  13268  dvdsrneg  13270  unitmulcl  13280  unitgrp  13283  unitnegcl  13297  subrguss  13355  subrgunit  13358  psmetsym  13799  psmettri  13800  mettri2  13832  xmetsym  13838  xmettri  13842  metrtri  13847  xblss2ps  13874  xblss2  13875  blhalf  13878  xmsge0  13937  cnmet  14000  ivthinclemlopn  14084  dveflem  14157  dvef  14158  sin0pilem1  14172  sinq12gt0  14221  sinq34lt0t  14222  cosq14gt0  14223  coseq0q4123  14225  rpabscxpbnd  14329  logbgcd1irraplemexp  14356  lgslem1  14371  lgseisenlem2  14421  2sqlem3  14434  2sqlem4  14435  2sqlem8  14440  pwf1oexmid  14719  qdencn  14745  cvgcmp2nlemabs  14750  apdifflemf  14764  apdifflemr  14765