Theorem breqtrd 4085

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

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4059

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  breqtrrd  4087  breqtrid  4096  tfrexlem  6443  phplem4  6977  phplem4on  6990  fidifsnen  6993  fisbth  7006  fin0  7008  fin0or  7009  ltsonq  7546  addlocprlemeqgt  7680  prmuloclemcalc  7713  mullocprlem  7718  addcanprlemu  7763  ltaprlem  7766  ltaprg  7767  prplnqu  7768  ltmprr  7790  cauappcvgprlemopl  7794  cauappcvgprlemloc  7800  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemloc  7823  caucvgprprlemloccalc  7832  caucvgprprlemopl  7845  recexgt0sr  7921  ltm1sr  7925  prsrpos  7933  caucvgsrlemoffgt1  7947  caucvgsr  7950  suplocsrlempr  7955  pitoregt0  7997  axpre-suploclemres  8049  add20  8582  mullt0  8588  ltmul1a  8699  ltm1  8954  recgt0  8958  prodgt0gt0  8959  prodgt0  8960  prodge0  8962  lemul1a  8966  recp1lt1  9007  recreclt  9008  ledivp1  9011  mulle0r  9052  ltaddrp2d  9888  mul2lt0np  9920  xleadd1a  10030  xleaddadd  10044  fz01en  10210  fzonmapblen  10348  qbtwnrelemcalc  10435  flqaddz  10477  flhalf  10482  flqdiv  10503  modqmuladdim  10549  modqsubdir  10575  addmodlteq  10580  frecfzen2  10609  iseqf1olemab  10684  ser3le  10719  ltexp2a  10773  leexp2a  10774  exple1  10777  expubnd  10778  bernneq  10842  faclbnd6  10926  hashfz  11003  zfz1isolemiso  11021  zfz1iso  11023  seq3coll  11024  cvg1nlemcxze  11408  cvg1nlemres  11411  recvguniqlem  11420  resqrexlemover  11436  resqrexlemdec  11437  resqrexlemcalc2  11441  resqrexlemcalc3  11442  resqrexlemnm  11444  resqrexlemoverl  11447  ltabs  11513  abslt  11514  absle  11515  abstri  11530  maxabslemlub  11633  maxabslemval  11634  dfabsmax  11643  bdtrilem  11665  xrmaxiflemab  11673  xrmaxiflemlub  11674  xrmaxaddlem  11686  reccn2ap  11739  climge0  11751  climaddc2  11756  summodclem2a  11807  zsumdc  11810  isumge0  11856  fsumle  11889  fsumlt  11890  isumshft  11916  expcnvap0  11928  geolim  11937  geolim2  11938  georeclim  11939  geo2lim  11942  cvgratnnlembern  11949  cvgratnnlemfm  11955  mertenslemi1  11961  mertensabs  11963  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  efcllemp  12084  ef0lem  12086  efgt0  12110  eftlub  12116  efltim  12124  sinbnd  12178  cosbnd  12179  ef01bndlem  12182  sin01gt0  12188  cos01gt0  12189  sin02gt0  12190  eirraplem  12203  dvdssub2  12261  dvdsadd2b  12266  dvdsexp  12287  3dvds  12290  opoe  12321  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  bitsfzolem  12380  bitsinv1lem  12387  gcdaddm  12420  bezoutlemstep  12433  dvdsgcd  12448  dvdsmulgcd  12461  bezoutr1  12469  nninfctlemfo  12476  nn0seqcvgd  12478  rpmulgcd2  12532  qredeq  12533  rpdvds  12536  prmind2  12557  divdenle  12634  phicl2  12651  hashdvds  12658  phimullem  12662  eulerthlemth  12669  prmdiveq  12673  prmdivdiv  12674  pythagtriplem4  12706  pythagtriplem10  12707  pythagtriplem19  12720  pcpre1  12730  pcadd2  12779  qexpz  12790  expnprm  12791  oddprmdvds  12792  pockthlem  12794  4sqlem7  12822  4sqlem10  12825  4sqexercise1  12836  4sqexercise2  12837  4sqlemsdc  12838  4sqlem11  12839  4sqlem12  12840  4sqlem14  12842  4sqlem15  12843  4sqlem16  12844  ennnfonelemkh  12898  ennnfonelemnn0  12908  qusgrp  13683  dvdsrid  13977  dvdsrtr  13978  dvdsrneg  13980  unitmulcl  13990  unitgrp  13993  unitnegcl  14007  subrguss  14113  subrgunit  14116  znidomb  14535  psmetsym  14916  psmettri  14917  mettri2  14949  xmetsym  14955  xmettri  14959  metrtri  14964  xblss2ps  14991  xblss2  14992  blhalf  14995  xmsge0  15054  cnmet  15117  ivthinclemlopn  15223  ivthdichlem  15238  dveflem  15313  dvef  15314  plyaddlem1  15334  sin0pilem1  15368  sinq12gt0  15417  sinq34lt0t  15418  cosq14gt0  15419  coseq0q4123  15421  rpabscxpbnd  15527  logbgcd1irraplemexp  15555  dvdsppwf1o  15576  mpodvdsmulf1o  15577  perfectlem2  15587  lgslem1  15592  lgseisenlem2  15663  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem1  15673  2sqlem3  15709  2sqlem4  15710  2sqlem8  15715  pwf1oexmid  16138  qdencn  16168  cvgcmp2nlemabs  16173  apdifflemf  16187  apdifflemr  16188