Theorem breqtrd 4071

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

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4045

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046

This theorem is referenced by:  breqtrrd  4073  breqtrid  4082  tfrexlem  6422  phplem4  6954  phplem4on  6966  fidifsnen  6969  fisbth  6982  fin0  6984  fin0or  6985  ltsonq  7513  addlocprlemeqgt  7647  prmuloclemcalc  7680  mullocprlem  7685  addcanprlemu  7730  ltaprlem  7733  ltaprg  7734  prplnqu  7735  ltmprr  7757  cauappcvgprlemopl  7761  cauappcvgprlemloc  7767  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemloc  7790  caucvgprprlemloccalc  7799  caucvgprprlemopl  7812  recexgt0sr  7888  ltm1sr  7892  prsrpos  7900  caucvgsrlemoffgt1  7914  caucvgsr  7917  suplocsrlempr  7922  pitoregt0  7964  axpre-suploclemres  8016  add20  8549  mullt0  8555  ltmul1a  8666  ltm1  8921  recgt0  8925  prodgt0gt0  8926  prodgt0  8927  prodge0  8929  lemul1a  8933  recp1lt1  8974  recreclt  8975  ledivp1  8978  mulle0r  9019  ltaddrp2d  9855  mul2lt0np  9887  xleadd1a  9997  xleaddadd  10011  fz01en  10177  fzonmapblen  10313  qbtwnrelemcalc  10400  flqaddz  10442  flhalf  10447  flqdiv  10468  modqmuladdim  10514  modqsubdir  10540  addmodlteq  10545  frecfzen2  10574  iseqf1olemab  10649  ser3le  10684  ltexp2a  10738  leexp2a  10739  exple1  10742  expubnd  10743  bernneq  10807  faclbnd6  10891  hashfz  10968  zfz1isolemiso  10986  zfz1iso  10988  seq3coll  10989  cvg1nlemcxze  11326  cvg1nlemres  11329  recvguniqlem  11338  resqrexlemover  11354  resqrexlemdec  11355  resqrexlemcalc2  11359  resqrexlemcalc3  11360  resqrexlemnm  11362  resqrexlemoverl  11365  ltabs  11431  abslt  11432  absle  11433  abstri  11448  maxabslemlub  11551  maxabslemval  11552  dfabsmax  11561  bdtrilem  11583  xrmaxiflemab  11591  xrmaxiflemlub  11592  xrmaxaddlem  11604  reccn2ap  11657  climge0  11669  climaddc2  11674  summodclem2a  11725  zsumdc  11728  isumge0  11774  fsumle  11807  fsumlt  11808  isumshft  11834  expcnvap0  11846  geolim  11855  geolim2  11856  georeclim  11857  geo2lim  11860  cvgratnnlembern  11867  cvgratnnlemfm  11873  mertenslemi1  11879  mertensabs  11881  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  efcllemp  12002  ef0lem  12004  efgt0  12028  eftlub  12034  efltim  12042  sinbnd  12096  cosbnd  12097  ef01bndlem  12100  sin01gt0  12106  cos01gt0  12107  sin02gt0  12108  eirraplem  12121  dvdssub2  12179  dvdsadd2b  12184  dvdsexp  12205  3dvds  12208  opoe  12239  divalglemeunn  12265  divalglemex  12266  divalglemeuneg  12267  bitsfzolem  12298  bitsinv1lem  12305  gcdaddm  12338  bezoutlemstep  12351  dvdsgcd  12366  dvdsmulgcd  12379  bezoutr1  12387  nninfctlemfo  12394  nn0seqcvgd  12396  rpmulgcd2  12450  qredeq  12451  rpdvds  12454  prmind2  12475  divdenle  12552  phicl2  12569  hashdvds  12576  phimullem  12580  eulerthlemth  12587  prmdiveq  12591  prmdivdiv  12592  pythagtriplem4  12624  pythagtriplem10  12625  pythagtriplem19  12638  pcpre1  12648  pcadd2  12697  qexpz  12708  expnprm  12709  oddprmdvds  12710  pockthlem  12712  4sqlem7  12740  4sqlem10  12743  4sqexercise1  12754  4sqexercise2  12755  4sqlemsdc  12756  4sqlem11  12757  4sqlem12  12758  4sqlem14  12760  4sqlem15  12761  4sqlem16  12762  ennnfonelemkh  12816  ennnfonelemnn0  12826  qusgrp  13601  dvdsrid  13895  dvdsrtr  13896  dvdsrneg  13898  unitmulcl  13908  unitgrp  13911  unitnegcl  13925  subrguss  14031  subrgunit  14034  znidomb  14453  psmetsym  14834  psmettri  14835  mettri2  14867  xmetsym  14873  xmettri  14877  metrtri  14882  xblss2ps  14909  xblss2  14910  blhalf  14913  xmsge0  14972  cnmet  15035  ivthinclemlopn  15141  ivthdichlem  15156  dveflem  15231  dvef  15232  plyaddlem1  15252  sin0pilem1  15286  sinq12gt0  15335  sinq34lt0t  15336  cosq14gt0  15337  coseq0q4123  15339  rpabscxpbnd  15445  logbgcd1irraplemexp  15473  dvdsppwf1o  15494  mpodvdsmulf1o  15495  perfectlem2  15505  lgslem1  15510  lgseisenlem2  15581  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem1  15591  2sqlem3  15627  2sqlem4  15628  2sqlem8  15633  pwf1oexmid  15973  qdencn  16003  cvgcmp2nlemabs  16008  apdifflemf  16022  apdifflemr  16023