Theorem breqtrd 4041

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

Syntax hints:   → wi 4   = wceq 1363   class class class wbr 4015

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-un 3145  df-sn 3610  df-pr 3611  df-op 3613  df-br 4016

This theorem is referenced by:  breqtrrd  4043  breqtrid  4052  tfrexlem  6348  phplem4  6868  phplem4on  6880  fidifsnen  6883  fisbth  6896  fin0  6898  fin0or  6899  ltsonq  7410  addlocprlemeqgt  7544  prmuloclemcalc  7577  mullocprlem  7582  addcanprlemu  7627  ltaprlem  7630  ltaprg  7631  prplnqu  7632  ltmprr  7654  cauappcvgprlemopl  7658  cauappcvgprlemloc  7664  cauappcvgprlemladdru  7668  cauappcvgprlemladdrl  7669  cauappcvgprlem1  7671  caucvgprlemm  7680  caucvgprlemopl  7681  caucvgprlemloc  7687  caucvgprprlemloccalc  7696  caucvgprprlemopl  7709  recexgt0sr  7785  ltm1sr  7789  prsrpos  7797  caucvgsrlemoffgt1  7811  caucvgsr  7814  suplocsrlempr  7819  pitoregt0  7861  axpre-suploclemres  7913  add20  8444  mullt0  8450  ltmul1a  8561  ltm1  8816  recgt0  8820  prodgt0gt0  8821  prodgt0  8822  prodge0  8824  lemul1a  8828  recp1lt1  8869  recreclt  8870  ledivp1  8873  mulle0r  8914  ltaddrp2d  9744  mul2lt0np  9776  xleadd1a  9886  xleaddadd  9900  fz01en  10066  fzonmapblen  10200  qbtwnrelemcalc  10269  flqaddz  10310  flhalf  10315  flqdiv  10334  modqmuladdim  10380  modqsubdir  10406  addmodlteq  10411  frecfzen2  10440  iseqf1olemab  10502  ser3le  10531  ltexp2a  10585  leexp2a  10586  exple1  10589  expubnd  10590  bernneq  10654  faclbnd6  10737  hashfz  10814  zfz1isolemiso  10832  zfz1iso  10834  seq3coll  10835  cvg1nlemcxze  11004  cvg1nlemres  11007  recvguniqlem  11016  resqrexlemover  11032  resqrexlemdec  11033  resqrexlemcalc2  11037  resqrexlemcalc3  11038  resqrexlemnm  11040  resqrexlemoverl  11043  ltabs  11109  abslt  11110  absle  11111  abstri  11126  maxabslemlub  11229  maxabslemval  11230  dfabsmax  11239  bdtrilem  11260  xrmaxiflemab  11268  xrmaxiflemlub  11269  xrmaxaddlem  11281  reccn2ap  11334  climge0  11346  climaddc2  11351  summodclem2a  11402  zsumdc  11405  isumge0  11451  fsumle  11484  fsumlt  11485  isumshft  11511  expcnvap0  11523  geolim  11532  geolim2  11533  georeclim  11534  geo2lim  11537  cvgratnnlembern  11544  cvgratnnlemfm  11550  mertenslemi1  11556  mertensabs  11558  prodmodclem3  11596  prodmodclem2a  11597  zproddc  11600  fprodseq  11604  efcllemp  11679  ef0lem  11681  efgt0  11705  eftlub  11711  efltim  11719  sinbnd  11773  cosbnd  11774  ef01bndlem  11777  sin01gt0  11782  cos01gt0  11783  sin02gt0  11784  eirraplem  11797  dvdssub2  11855  dvdsadd2b  11860  dvdsexp  11880  opoe  11913  divalglemeunn  11939  divalglemex  11940  divalglemeuneg  11941  gcdaddm  11998  bezoutlemstep  12011  dvdsgcd  12026  dvdsmulgcd  12039  bezoutr1  12047  nn0seqcvgd  12054  rpmulgcd2  12108  qredeq  12109  rpdvds  12112  prmind2  12133  divdenle  12210  phicl2  12227  hashdvds  12234  phimullem  12238  eulerthlemth  12245  prmdiveq  12249  prmdivdiv  12250  pythagtriplem4  12281  pythagtriplem10  12282  pythagtriplem19  12295  pcpre1  12305  qexpz  12363  expnprm  12364  oddprmdvds  12365  pockthlem  12367  4sqlem7  12395  4sqlem10  12398  ennnfonelemkh  12426  ennnfonelemnn0  12436  dvdsrid  13343  dvdsrtr  13344  dvdsrneg  13346  unitmulcl  13356  unitgrp  13359  unitnegcl  13373  subrguss  13451  subrgunit  13454  psmetsym  14100  psmettri  14101  mettri2  14133  xmetsym  14139  xmettri  14143  metrtri  14148  xblss2ps  14175  xblss2  14176  blhalf  14179  xmsge0  14238  cnmet  14301  ivthinclemlopn  14385  dveflem  14458  dvef  14459  sin0pilem1  14473  sinq12gt0  14522  sinq34lt0t  14523  cosq14gt0  14524  coseq0q4123  14526  rpabscxpbnd  14630  logbgcd1irraplemexp  14657  lgslem1  14672  lgseisenlem2  14722  2sqlem3  14735  2sqlem4  14736  2sqlem8  14741  pwf1oexmid  15021  qdencn  15047  cvgcmp2nlemabs  15052  apdifflemf  15066  apdifflemr  15067