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  10426  qbtwnrelemcalc  10515  flqaddz  10557  flhalf  10562  flqdiv  10583  modqmuladdim  10629  modqsubdir  10655  addmodlteq  10660  frecfzen2  10689  iseqf1olemab  10764  ser3le  10799  ltexp2a  10853  leexp2a  10854  exple1  10857  expubnd  10858  bernneq  10922  faclbnd6  11006  hashfz  11085  zfz1isolemiso  11103  zfz1iso  11105  seq3coll  11106  cvg1nlemcxze  11543  cvg1nlemres  11546  recvguniqlem  11555  resqrexlemover  11571  resqrexlemdec  11572  resqrexlemcalc2  11576  resqrexlemcalc3  11577  resqrexlemnm  11579  resqrexlemoverl  11582  ltabs  11648  abslt  11649  absle  11650  abstri  11665  maxabslemlub  11768  maxabslemval  11769  dfabsmax  11778  bdtrilem  11800  xrmaxiflemab  11808  xrmaxiflemlub  11809  xrmaxaddlem  11821  reccn2ap  11874  climge0  11886  climaddc2  11891  summodclem2a  11943  zsumdc  11946  isumge0  11992  fsumle  12025  fsumlt  12026  isumshft  12052  expcnvap0  12064  geolim  12073  geolim2  12074  georeclim  12075  geo2lim  12078  cvgratnnlembern  12085  cvgratnnlemfm  12091  mertenslemi1  12097  mertensabs  12099  prodmodclem3  12137  prodmodclem2a  12138  zproddc  12141  fprodseq  12145  efcllemp  12220  ef0lem  12222  efgt0  12246  eftlub  12252  efltim  12260  sinbnd  12314  cosbnd  12315  ef01bndlem  12318  sin01gt0  12324  cos01gt0  12325  sin02gt0  12326  eirraplem  12339  dvdssub2  12397  dvdsadd2b  12402  dvdsexp  12423  3dvds  12426  opoe  12457  divalglemeunn  12483  divalglemex  12484  divalglemeuneg  12485  bitsfzolem  12516  bitsinv1lem  12523  gcdaddm  12556  bezoutlemstep  12569  dvdsgcd  12584  dvdsmulgcd  12597  bezoutr1  12605  nninfctlemfo  12612  nn0seqcvgd  12614  rpmulgcd2  12668  qredeq  12669  rpdvds  12672  prmind2  12693  divdenle  12770  phicl2  12787  hashdvds  12794  phimullem  12798  eulerthlemth  12805  prmdiveq  12809  prmdivdiv  12810  pythagtriplem4  12842  pythagtriplem10  12843  pythagtriplem19  12856  pcpre1  12866  pcadd2  12915  qexpz  12926  expnprm  12927  oddprmdvds  12928  pockthlem  12930  4sqlem7  12958  4sqlem10  12961  4sqexercise1  12972  4sqexercise2  12973  4sqlemsdc  12974  4sqlem11  12975  4sqlem12  12976  4sqlem14  12978  4sqlem15  12979  4sqlem16  12980  ennnfonelemkh  13034  ennnfonelemnn0  13044  qusgrp  13820  dvdsrid  14116  dvdsrtr  14117  dvdsrneg  14119  unitmulcl  14129  unitgrp  14132  unitnegcl  14146  subrguss  14252  subrgunit  14255  znidomb  14674  psmetsym  15055  psmettri  15056  mettri2  15088  xmetsym  15094  xmettri  15098  metrtri  15103  xblss2ps  15130  xblss2  15131  blhalf  15134  xmsge0  15193  cnmet  15256  ivthinclemlopn  15362  ivthdichlem  15377  dveflem  15452  dvef  15453  plyaddlem1  15473  sin0pilem1  15507  sinq12gt0  15556  sinq34lt0t  15557  cosq14gt0  15558  coseq0q4123  15560  rpabscxpbnd  15666  logbgcd1irraplemexp  15694  dvdsppwf1o  15715  mpodvdsmulf1o  15716  perfectlem2  15726  lgslem1  15731  lgseisenlem2  15802  lgsquadlem1  15808  lgsquadlem2  15809  lgsquad2lem1  15812  2sqlem3  15848  2sqlem4  15849  2sqlem8  15854  pwf1oexmid  16603  qdencn  16634  cvgcmp2nlemabs  16639  apdifflemf  16653  apdifflemr  16654