Theorem breqtrd 4119

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  breqtrrd  4121  breqtrid  4130  tfrexlem  6543  phplem4  7084  phplem4on  7097  fidifsnen  7100  fisbth  7115  fin0  7117  fin0or  7118  ltsonq  7678  addlocprlemeqgt  7812  prmuloclemcalc  7845  mullocprlem  7850  addcanprlemu  7895  ltaprlem  7898  ltaprg  7899  prplnqu  7900  ltmprr  7922  cauappcvgprlemopl  7926  cauappcvgprlemloc  7932  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem1  7939  caucvgprlemm  7948  caucvgprlemopl  7949  caucvgprlemloc  7955  caucvgprprlemloccalc  7964  caucvgprprlemopl  7977  recexgt0sr  8053  ltm1sr  8057  prsrpos  8065  caucvgsrlemoffgt1  8079  caucvgsr  8082  suplocsrlempr  8087  pitoregt0  8129  axpre-suploclemres  8181  add20  8713  mullt0  8719  ltmul1a  8830  ltm1  9085  recgt0  9089  prodgt0gt0  9090  prodgt0  9091  prodge0  9093  lemul1a  9097  recp1lt1  9138  recreclt  9139  ledivp1  9142  mulle0r  9183  eluzmn  9823  ltaddrp2d  10027  mul2lt0np  10059  xleadd1a  10169  xleaddadd  10183  lincmble  10300  fz01en  10350  fzonmapblen  10489  qbtwnrelemcalc  10578  flqaddz  10620  flhalf  10625  flqdiv  10646  modqmuladdim  10692  modqsubdir  10718  addmodlteq  10723  frecfzen2  10752  iseqf1olemab  10827  ser3le  10862  ltexp2a  10916  leexp2a  10917  exple1  10920  expubnd  10921  bernneq  10985  faclbnd6  11069  hashfz  11148  zfz1isolemiso  11166  zfz1iso  11168  seq3coll  11169  cvg1nlemcxze  11622  cvg1nlemres  11625  recvguniqlem  11634  resqrexlemover  11650  resqrexlemdec  11651  resqrexlemcalc2  11655  resqrexlemcalc3  11656  resqrexlemnm  11658  resqrexlemoverl  11661  ltabs  11727  abslt  11728  absle  11729  abstri  11744  maxabslemlub  11847  maxabslemval  11848  dfabsmax  11857  bdtrilem  11879  xrmaxiflemab  11887  xrmaxiflemlub  11888  xrmaxaddlem  11900  reccn2ap  11953  climge0  11965  climaddc2  11970  summodclem2a  12022  zsumdc  12025  isumge0  12071  fsumle  12104  fsumlt  12105  isumshft  12131  expcnvap0  12143  geolim  12152  geolim2  12153  georeclim  12154  geo2lim  12157  cvgratnnlembern  12164  cvgratnnlemfm  12170  mertenslemi1  12176  mertensabs  12178  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  efcllemp  12299  ef0lem  12301  efgt0  12325  eftlub  12331  efltim  12339  sinbnd  12393  cosbnd  12394  ef01bndlem  12397  sin01gt0  12403  cos01gt0  12404  sin02gt0  12405  eirraplem  12418  dvdssub2  12476  dvdsadd2b  12481  dvdsexp  12502  3dvds  12505  opoe  12536  divalglemeunn  12562  divalglemex  12563  divalglemeuneg  12564  bitsfzolem  12595  bitsinv1lem  12602  gcdaddm  12635  bezoutlemstep  12648  dvdsgcd  12663  dvdsmulgcd  12676  bezoutr1  12684  nninfctlemfo  12691  nn0seqcvgd  12693  rpmulgcd2  12747  qredeq  12748  rpdvds  12751  prmind2  12772  divdenle  12849  phicl2  12866  hashdvds  12873  phimullem  12877  eulerthlemth  12884  prmdiveq  12888  prmdivdiv  12889  pythagtriplem4  12921  pythagtriplem10  12922  pythagtriplem19  12935  pcpre1  12945  pcadd2  12994  qexpz  13005  expnprm  13006  oddprmdvds  13007  pockthlem  13009  4sqlem7  13037  4sqlem10  13040  4sqexercise1  13051  4sqexercise2  13052  4sqlemsdc  13053  4sqlem11  13054  4sqlem12  13055  4sqlem14  13057  4sqlem15  13058  4sqlem16  13059  ennnfonelemkh  13113  ennnfonelemnn0  13123  qusgrp  13899  dvdsrid  14195  dvdsrtr  14196  dvdsrneg  14198  unitmulcl  14208  unitgrp  14211  unitnegcl  14225  subrguss  14331  subrgunit  14334  znidomb  14754  psmetsym  15140  psmettri  15141  mettri2  15173  xmetsym  15179  xmettri  15183  metrtri  15188  xblss2ps  15215  xblss2  15216  blhalf  15219  xmsge0  15278  cnmet  15341  ivthinclemlopn  15447  ivthdichlem  15462  dveflem  15537  dvef  15538  plyaddlem1  15558  sin0pilem1  15592  sinq12gt0  15641  sinq34lt0t  15642  cosq14gt0  15643  coseq0q4123  15645  rpabscxpbnd  15751  logbgcd1irraplemexp  15779  dvdsppwf1o  15803  mpodvdsmulf1o  15804  perfectlem2  15814  lgslem1  15819  lgseisenlem2  15890  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem1  15900  2sqlem3  15936  2sqlem4  15937  2sqlem8  15942  pwf1oexmid  16721  qdencn  16755  cvgcmp2nlemabs  16764  apdifflemf  16778  apdifflemr  16779