Theorem breqtrd 4114

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

Syntax hints:   → wi 4   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  breqtrrd  4116  breqtrid  4125  tfrexlem  6499  phplem4  7040  phplem4on  7053  fidifsnen  7056  fisbth  7071  fin0  7073  fin0or  7074  ltsonq  7617  addlocprlemeqgt  7751  prmuloclemcalc  7784  mullocprlem  7789  addcanprlemu  7834  ltaprlem  7837  ltaprg  7838  prplnqu  7839  ltmprr  7861  cauappcvgprlemopl  7865  cauappcvgprlemloc  7871  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemloc  7894  caucvgprprlemloccalc  7903  caucvgprprlemopl  7916  recexgt0sr  7992  ltm1sr  7996  prsrpos  8004  caucvgsrlemoffgt1  8018  caucvgsr  8021  suplocsrlempr  8026  pitoregt0  8068  axpre-suploclemres  8120  add20  8653  mullt0  8659  ltmul1a  8770  ltm1  9025  recgt0  9029  prodgt0gt0  9030  prodgt0  9031  prodge0  9033  lemul1a  9037  recp1lt1  9078  recreclt  9079  ledivp1  9082  mulle0r  9123  eluzmn  9761  ltaddrp2d  9965  mul2lt0np  9997  xleadd1a  10107  xleaddadd  10121  fz01en  10287  fzonmapblen  10425  qbtwnrelemcalc  10514  flqaddz  10556  flhalf  10561  flqdiv  10582  modqmuladdim  10628  modqsubdir  10654  addmodlteq  10659  frecfzen2  10688  iseqf1olemab  10763  ser3le  10798  ltexp2a  10852  leexp2a  10853  exple1  10856  expubnd  10857  bernneq  10921  faclbnd6  11005  hashfz  11084  zfz1isolemiso  11102  zfz1iso  11104  seq3coll  11105  cvg1nlemcxze  11542  cvg1nlemres  11545  recvguniqlem  11554  resqrexlemover  11570  resqrexlemdec  11571  resqrexlemcalc2  11575  resqrexlemcalc3  11576  resqrexlemnm  11578  resqrexlemoverl  11581  ltabs  11647  abslt  11648  absle  11649  abstri  11664  maxabslemlub  11767  maxabslemval  11768  dfabsmax  11777  bdtrilem  11799  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxaddlem  11820  reccn2ap  11873  climge0  11885  climaddc2  11890  summodclem2a  11941  zsumdc  11944  isumge0  11990  fsumle  12023  fsumlt  12024  isumshft  12050  expcnvap0  12062  geolim  12071  geolim2  12072  georeclim  12073  geo2lim  12076  cvgratnnlembern  12083  cvgratnnlemfm  12089  mertenslemi1  12095  mertensabs  12097  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  efcllemp  12218  ef0lem  12220  efgt0  12244  eftlub  12250  efltim  12258  sinbnd  12312  cosbnd  12313  ef01bndlem  12316  sin01gt0  12322  cos01gt0  12323  sin02gt0  12324  eirraplem  12337  dvdssub2  12395  dvdsadd2b  12400  dvdsexp  12421  3dvds  12424  opoe  12455  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  bitsfzolem  12514  bitsinv1lem  12521  gcdaddm  12554  bezoutlemstep  12567  dvdsgcd  12582  dvdsmulgcd  12595  bezoutr1  12603  nninfctlemfo  12610  nn0seqcvgd  12612  rpmulgcd2  12666  qredeq  12667  rpdvds  12670  prmind2  12691  divdenle  12768  phicl2  12785  hashdvds  12792  phimullem  12796  eulerthlemth  12803  prmdiveq  12807  prmdivdiv  12808  pythagtriplem4  12840  pythagtriplem10  12841  pythagtriplem19  12854  pcpre1  12864  pcadd2  12913  qexpz  12924  expnprm  12925  oddprmdvds  12926  pockthlem  12928  4sqlem7  12956  4sqlem10  12959  4sqexercise1  12970  4sqexercise2  12971  4sqlemsdc  12972  4sqlem11  12973  4sqlem12  12974  4sqlem14  12976  4sqlem15  12977  4sqlem16  12978  ennnfonelemkh  13032  ennnfonelemnn0  13042  qusgrp  13818  dvdsrid  14113  dvdsrtr  14114  dvdsrneg  14116  unitmulcl  14126  unitgrp  14129  unitnegcl  14143  subrguss  14249  subrgunit  14252  znidomb  14671  psmetsym  15052  psmettri  15053  mettri2  15085  xmetsym  15091  xmettri  15095  metrtri  15100  xblss2ps  15127  xblss2  15128  blhalf  15131  xmsge0  15190  cnmet  15253  ivthinclemlopn  15359  ivthdichlem  15374  dveflem  15449  dvef  15450  plyaddlem1  15470  sin0pilem1  15504  sinq12gt0  15553  sinq34lt0t  15554  cosq14gt0  15555  coseq0q4123  15557  rpabscxpbnd  15663  logbgcd1irraplemexp  15691  dvdsppwf1o  15712  mpodvdsmulf1o  15713  perfectlem2  15723  lgslem1  15728  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem1  15809  2sqlem3  15845  2sqlem4  15846  2sqlem8  15851  pwf1oexmid  16600  qdencn  16631  cvgcmp2nlemabs  16636  apdifflemf  16650  apdifflemr  16651