Theorem breqtrd 4140

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

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4114

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  breqtrrd  4142  breqtrid  4151  tfrexlem  6578  phplem4  7122  phplem4on  7135  fidifsnen  7138  fisbth  7153  fin0  7155  fin0or  7156  ltsonq  7729  addlocprlemeqgt  7863  prmuloclemcalc  7896  mullocprlem  7901  addcanprlemu  7946  ltaprlem  7949  ltaprg  7950  prplnqu  7951  ltmprr  7973  cauappcvgprlemopl  7977  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemloc  8006  caucvgprprlemloccalc  8015  caucvgprprlemopl  8028  recexgt0sr  8104  ltm1sr  8108  prsrpos  8116  caucvgsrlemoffgt1  8130  caucvgsr  8133  suplocsrlempr  8138  pitoregt0  8180  axpre-suploclemres  8232  add20  8765  mullt0  8771  ltmul1a  8882  ltm1  9137  recgt0  9141  prodgt0gt0  9142  prodgt0  9143  prodge0  9145  lemul1a  9149  recp1lt1  9190  recreclt  9191  ledivp1  9194  mulle0r  9235  eluzmn  9878  ltaddrp2d  10082  mul2lt0np  10114  xleadd1a  10225  xleaddadd  10239  lincmble  10356  fz01en  10408  fzonmapblen  10548  qbtwnrelemcalc  10639  flqaddz  10681  flhalf  10686  flqdiv  10707  modqmuladdim  10753  modqsubdir  10779  addmodlteq  10784  frecfzen2  10813  iseqf1olemab  10888  ser3le  10923  ltexp2a  10977  leexp2a  10978  exple1  10981  expubnd  10982  bernneq  11047  faclbnd6  11131  hashfz  11211  zfz1isolemiso  11236  zfz1iso  11238  seq3coll  11239  cvg1nlemcxze  11692  cvg1nlemres  11695  recvguniqlem  11704  resqrexlemover  11720  resqrexlemdec  11721  resqrexlemcalc2  11725  resqrexlemcalc3  11726  resqrexlemnm  11728  resqrexlemoverl  11731  ltabs  11797  abslt  11798  absle  11799  abstri  11814  maxabslemlub  11917  maxabslemval  11918  dfabsmax  11927  bdtrilem  11949  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxaddlem  11970  reccn2ap  12023  climge0  12035  climaddc2  12040  summodclem2a  12092  zsumdc  12095  isumge0  12141  fsumle  12174  fsumlt  12175  isumshft  12201  expcnvap0  12213  geolim  12222  geolim2  12223  georeclim  12224  geo2lim  12227  cvgratnnlembern  12234  cvgratnnlemfm  12240  mertenslemi1  12246  mertensabs  12248  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  efcllemp  12369  ef0lem  12371  efgt0  12395  eftlub  12401  efltim  12409  sinbnd  12463  cosbnd  12464  ef01bndlem  12467  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  eirraplem  12488  dvdssub2  12546  dvdsadd2b  12551  dvdsexp  12572  3dvds  12575  opoe  12606  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  bitsfzolem  12665  bitsinv1lem  12672  gcdaddm  12705  bezoutlemstep  12718  dvdsgcd  12733  dvdsmulgcd  12746  bezoutr1  12754  nninfctlemfo  12761  nn0seqcvgd  12763  rpmulgcd2  12817  qredeq  12818  rpdvds  12821  prmind2  12842  divdenle  12919  phicl2  12936  hashdvds  12943  phimullem  12947  eulerthlemth  12954  prmdiveq  12958  prmdivdiv  12959  pythagtriplem4  12991  pythagtriplem10  12992  pythagtriplem19  13005  pcpre1  13015  pcadd2  13064  qexpz  13075  expnprm  13076  oddprmdvds  13077  pockthlem  13079  4sqlem7  13107  4sqlem10  13110  4sqexercise1  13121  4sqexercise2  13122  4sqlemsdc  13123  4sqlem11  13124  4sqlem12  13125  4sqlem14  13127  4sqlem15  13128  4sqlem16  13129  ennnfonelemkh  13247  ennnfonelemnn0  13257  qusgrp  13985  dvdsrid  14345  dvdsrtr  14346  dvdsrneg  14348  unitmulcl  14358  unitgrp  14361  unitnegcl  14375  subrguss  14482  subrgunit  14485  znidomb  14932  psmetsym  15320  psmettri  15321  mettri2  15353  xmetsym  15359  xmettri  15363  metrtri  15368  xblss2ps  15395  xblss2  15396  blhalf  15399  xmsge0  15458  cnmet  15521  ivthinclemlopn  15627  ivthdichlem  15642  dveflem  15717  dvef  15718  plyaddlem1  15738  sin0pilem1  15772  sinq12gt0  15821  sinq34lt0t  15822  cosq14gt0  15823  coseq0q4123  15825  rpabscxpbnd  15931  logbgcd1irraplemexp  15959  dvdsppwf1o  15983  mpodvdsmulf1o  15984  perfectlem2  15994  lgslem1  15999  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem1  16080  2sqlem3  16116  2sqlem4  16117  2sqlem8  16122  pwf1oexmid  16899  qdencn  16933  cvgcmp2nlemabs  16942  apdifflemf  16956  apdifflemr  16957