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  6500  phplem4  7041  phplem4on  7054  fidifsnen  7057  fisbth  7072  fin0  7074  fin0or  7075  ltsonq  7618  addlocprlemeqgt  7752  prmuloclemcalc  7785  mullocprlem  7790  addcanprlemu  7835  ltaprlem  7838  ltaprg  7839  prplnqu  7840  ltmprr  7862  cauappcvgprlemopl  7866  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemloc  7895  caucvgprprlemloccalc  7904  caucvgprprlemopl  7917  recexgt0sr  7993  ltm1sr  7997  prsrpos  8005  caucvgsrlemoffgt1  8019  caucvgsr  8022  suplocsrlempr  8027  pitoregt0  8069  axpre-suploclemres  8121  add20  8654  mullt0  8660  ltmul1a  8771  ltm1  9026  recgt0  9030  prodgt0gt0  9031  prodgt0  9032  prodge0  9034  lemul1a  9038  recp1lt1  9079  recreclt  9080  ledivp1  9083  mulle0r  9124  eluzmn  9762  ltaddrp2d  9966  mul2lt0np  9998  xleadd1a  10108  xleaddadd  10122  fz01en  10288  fzonmapblen  10427  qbtwnrelemcalc  10516  flqaddz  10558  flhalf  10563  flqdiv  10584  modqmuladdim  10630  modqsubdir  10656  addmodlteq  10661  frecfzen2  10690  iseqf1olemab  10765  ser3le  10800  ltexp2a  10854  leexp2a  10855  exple1  10858  expubnd  10859  bernneq  10923  faclbnd6  11007  hashfz  11086  zfz1isolemiso  11104  zfz1iso  11106  seq3coll  11107  cvg1nlemcxze  11560  cvg1nlemres  11563  recvguniqlem  11572  resqrexlemover  11588  resqrexlemdec  11589  resqrexlemcalc2  11593  resqrexlemcalc3  11594  resqrexlemnm  11596  resqrexlemoverl  11599  ltabs  11665  abslt  11666  absle  11667  abstri  11682  maxabslemlub  11785  maxabslemval  11786  dfabsmax  11795  bdtrilem  11817  xrmaxiflemab  11825  xrmaxiflemlub  11826  xrmaxaddlem  11838  reccn2ap  11891  climge0  11903  climaddc2  11908  summodclem2a  11960  zsumdc  11963  isumge0  12009  fsumle  12042  fsumlt  12043  isumshft  12069  expcnvap0  12081  geolim  12090  geolim2  12091  georeclim  12092  geo2lim  12095  cvgratnnlembern  12102  cvgratnnlemfm  12108  mertenslemi1  12114  mertensabs  12116  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  efcllemp  12237  ef0lem  12239  efgt0  12263  eftlub  12269  efltim  12277  sinbnd  12331  cosbnd  12332  ef01bndlem  12335  sin01gt0  12341  cos01gt0  12342  sin02gt0  12343  eirraplem  12356  dvdssub2  12414  dvdsadd2b  12419  dvdsexp  12440  3dvds  12443  opoe  12474  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  bitsfzolem  12533  bitsinv1lem  12540  gcdaddm  12573  bezoutlemstep  12586  dvdsgcd  12601  dvdsmulgcd  12614  bezoutr1  12622  nninfctlemfo  12629  nn0seqcvgd  12631  rpmulgcd2  12685  qredeq  12686  rpdvds  12689  prmind2  12710  divdenle  12787  phicl2  12804  hashdvds  12811  phimullem  12815  eulerthlemth  12822  prmdiveq  12826  prmdivdiv  12827  pythagtriplem4  12859  pythagtriplem10  12860  pythagtriplem19  12873  pcpre1  12883  pcadd2  12932  qexpz  12943  expnprm  12944  oddprmdvds  12945  pockthlem  12947  4sqlem7  12975  4sqlem10  12978  4sqexercise1  12989  4sqexercise2  12990  4sqlemsdc  12991  4sqlem11  12992  4sqlem12  12993  4sqlem14  12995  4sqlem15  12996  4sqlem16  12997  ennnfonelemkh  13051  ennnfonelemnn0  13061  qusgrp  13837  dvdsrid  14133  dvdsrtr  14134  dvdsrneg  14136  unitmulcl  14146  unitgrp  14149  unitnegcl  14163  subrguss  14269  subrgunit  14272  znidomb  14691  psmetsym  15072  psmettri  15073  mettri2  15105  xmetsym  15111  xmettri  15115  metrtri  15120  xblss2ps  15147  xblss2  15148  blhalf  15151  xmsge0  15210  cnmet  15273  ivthinclemlopn  15379  ivthdichlem  15394  dveflem  15469  dvef  15470  plyaddlem1  15490  sin0pilem1  15524  sinq12gt0  15573  sinq34lt0t  15574  cosq14gt0  15575  coseq0q4123  15577  rpabscxpbnd  15683  logbgcd1irraplemexp  15711  dvdsppwf1o  15732  mpodvdsmulf1o  15733  perfectlem2  15743  lgslem1  15748  lgseisenlem2  15819  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem1  15829  2sqlem3  15865  2sqlem4  15866  2sqlem8  15871  pwf1oexmid  16651  qdencn  16682  cvgcmp2nlemabs  16687  apdifflemf  16701  apdifflemr  16702