Theorem breqtrd 4135

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110

This theorem is referenced by:  breqtrrd  4137  breqtrid  4146  tfrexlem  6565  phplem4  7109  phplem4on  7122  fidifsnen  7125  fisbth  7140  fin0  7142  fin0or  7143  ltsonq  7713  addlocprlemeqgt  7847  prmuloclemcalc  7880  mullocprlem  7885  addcanprlemu  7930  ltaprlem  7933  ltaprg  7934  prplnqu  7935  ltmprr  7957  cauappcvgprlemopl  7961  cauappcvgprlemloc  7967  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemloc  7990  caucvgprprlemloccalc  7999  caucvgprprlemopl  8012  recexgt0sr  8088  ltm1sr  8092  prsrpos  8100  caucvgsrlemoffgt1  8114  caucvgsr  8117  suplocsrlempr  8122  pitoregt0  8164  axpre-suploclemres  8216  add20  8748  mullt0  8754  ltmul1a  8865  ltm1  9120  recgt0  9124  prodgt0gt0  9125  prodgt0  9126  prodge0  9128  lemul1a  9132  recp1lt1  9173  recreclt  9174  ledivp1  9177  mulle0r  9218  eluzmn  9860  ltaddrp2d  10064  mul2lt0np  10096  xleadd1a  10206  xleaddadd  10220  lincmble  10337  fz01en  10387  fzonmapblen  10526  qbtwnrelemcalc  10615  flqaddz  10657  flhalf  10662  flqdiv  10683  modqmuladdim  10729  modqsubdir  10755  addmodlteq  10760  frecfzen2  10789  iseqf1olemab  10864  ser3le  10899  ltexp2a  10953  leexp2a  10954  exple1  10957  expubnd  10958  bernneq  11022  faclbnd6  11106  hashfz  11186  zfz1isolemiso  11211  zfz1iso  11213  seq3coll  11214  cvg1nlemcxze  11667  cvg1nlemres  11670  recvguniqlem  11679  resqrexlemover  11695  resqrexlemdec  11696  resqrexlemcalc2  11700  resqrexlemcalc3  11701  resqrexlemnm  11703  resqrexlemoverl  11706  ltabs  11772  abslt  11773  absle  11774  abstri  11789  maxabslemlub  11892  maxabslemval  11893  dfabsmax  11902  bdtrilem  11924  xrmaxiflemab  11932  xrmaxiflemlub  11933  xrmaxaddlem  11945  reccn2ap  11998  climge0  12010  climaddc2  12015  summodclem2a  12067  zsumdc  12070  isumge0  12116  fsumle  12149  fsumlt  12150  isumshft  12176  expcnvap0  12188  geolim  12197  geolim2  12198  georeclim  12199  geo2lim  12202  cvgratnnlembern  12209  cvgratnnlemfm  12215  mertenslemi1  12221  mertensabs  12223  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  efcllemp  12344  ef0lem  12346  efgt0  12370  eftlub  12376  efltim  12384  sinbnd  12438  cosbnd  12439  ef01bndlem  12442  sin01gt0  12448  cos01gt0  12449  sin02gt0  12450  eirraplem  12463  dvdssub2  12521  dvdsadd2b  12526  dvdsexp  12547  3dvds  12550  opoe  12581  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  bitsfzolem  12640  bitsinv1lem  12647  gcdaddm  12680  bezoutlemstep  12693  dvdsgcd  12708  dvdsmulgcd  12721  bezoutr1  12729  nninfctlemfo  12736  nn0seqcvgd  12738  rpmulgcd2  12792  qredeq  12793  rpdvds  12796  prmind2  12817  divdenle  12894  phicl2  12911  hashdvds  12918  phimullem  12922  eulerthlemth  12929  prmdiveq  12933  prmdivdiv  12934  pythagtriplem4  12966  pythagtriplem10  12967  pythagtriplem19  12980  pcpre1  12990  pcadd2  13039  qexpz  13050  expnprm  13051  oddprmdvds  13052  pockthlem  13054  4sqlem7  13082  4sqlem10  13085  4sqexercise1  13096  4sqexercise2  13097  4sqlemsdc  13098  4sqlem11  13099  4sqlem12  13100  4sqlem14  13102  4sqlem15  13103  4sqlem16  13104  ennnfonelemkh  13163  ennnfonelemnn0  13173  qusgrp  13949  dvdsrid  14245  dvdsrtr  14246  dvdsrneg  14248  unitmulcl  14258  unitgrp  14261  unitnegcl  14275  subrguss  14381  subrgunit  14384  znidomb  14806  psmetsym  15194  psmettri  15195  mettri2  15227  xmetsym  15233  xmettri  15237  metrtri  15242  xblss2ps  15269  xblss2  15270  blhalf  15273  xmsge0  15332  cnmet  15395  ivthinclemlopn  15501  ivthdichlem  15516  dveflem  15591  dvef  15592  plyaddlem1  15612  sin0pilem1  15646  sinq12gt0  15695  sinq34lt0t  15696  cosq14gt0  15697  coseq0q4123  15699  rpabscxpbnd  15805  logbgcd1irraplemexp  15833  dvdsppwf1o  15857  mpodvdsmulf1o  15858  perfectlem2  15868  lgslem1  15873  lgseisenlem2  15944  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem1  15954  2sqlem3  15990  2sqlem4  15991  2sqlem8  15996  pwf1oexmid  16773  qdencn  16807  cvgcmp2nlemabs  16816  apdifflemf  16830  apdifflemr  16831