Theorem breqtrrd 4116

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
breqtrrd.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
breqtrrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrd

Step	Hyp	Ref	Expression
1		breqtrrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2237	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrd 4114	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:  frirrg  4447  fidcen  7087  unsnfidcex  7111  unsnfidcel  7112  addlocprlemeq  7752  ltexprlemopl  7820  recexprlemloc  7850  cauappcvgprlemopl  7865  cauappcvgprlemladdfu  7873  cauappcvgprlem1  7878  caucvgprlemopl  7888  caucvgprlemladdfu  7896  caucvgprprlemopl  7916  caucvgprprlemexbt  7925  mulgt0sr  7997  archsr  8001  caucvgsrlemoffgt1  8018  suplocsrlemb  8025  suplocsrlem  8027  mulap0r  8794  prodgt0  9031  div4p1lem1div2  9397  mul2lt0rgt0  9994  xnn0dcle  10036  xnn0letri  10037  xleadd1a  10107  xltadd1  10110  xlt2add  10114  xposdif  10116  xlesubadd  10117  xleaddadd  10121  uzsubsubfz  10281  fzctr  10367  subfzo0  10487  exbtwnzlemstep  10506  exbtwnzlemex  10508  rebtwn2zlemstep  10511  rebtwn2z  10513  qbtwnxr  10516  xqltnle  10526  fldiv4lem1div2uz2  10565  ceilqge  10571  modqge0  10593  modqlt  10594  modqid  10610  m1modge3gt1  10632  modaddmodup  10648  addmodlteq  10659  ser3mono  10748  seqf1oglem1  10780  seqf1oglem2  10781  ser3ge0  10797  ser3le  10798  leexp1a  10855  sqgt0ap  10869  sqge0  10877  nnlesq  10904  expnbnd  10924  nn0opthlem2d  10982  facwordi  11001  filtinf  11052  hashunlem  11066  zfz1isolemiso  11102  cats1fvd  11346  cjmulge0  11449  resqrexlemover  11570  resqrexlemdec  11571  resqrexlemlo  11573  resqrexlemcalc3  11576  resqrexlemcvg  11579  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemga  11583  absge0  11620  amgm2  11678  maxle1  11771  bdtrilem  11799  xrmaxifle  11806  xrmaxiflemlub  11808  xrmaxiflemval  11810  xrmax1sup  11813  xrmaxltsup  11818  xrmaxadd  11821  xrbdtri  11836  reccn2ap  11873  climle  11894  climserle  11905  isumclim2  11982  isumclim3  11983  isumge0  11990  fsumlessfi  12020  expcnvap0  12062  expcnvre  12063  explecnv  12065  absltap  12069  cvgratnnlembern  12083  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratnnlemabsle  12087  cvgratnnlemfm  12089  cvgratnnlemrate  12090  mertenslemi1  12095  mertenslem2  12096  clim2divap  12100  prodmodclem3  12135  efcvg  12226  ege2le3  12231  efaddlem  12234  eftlub  12250  effsumlt  12252  ef01bndlem  12316  sin02gt0  12324  eirrap  12338  iddvdsexp  12375  dvdsadd  12396  dvdsfac  12420  dvdsmod  12422  3dvds  12424  omoe  12456  divalglemnn  12478  divalglemnqt  12480  flodddiv4t2lthalf  12499  bitsfzo  12515  bitsmod  12516  bitscmp  12518  bitsinv1lem  12521  dvdslegcd  12534  dfgcd3  12580  dvdssqim  12594  dvdsmulgcd  12595  nn0seqcvgd  12612  dvdslcm  12640  lcmgcdlem  12648  mulgcddvds  12665  qredeq  12667  cncongr2  12675  sqnprm  12707  isprm6  12718  sqpweven  12746  znege1  12749  sqrt2irrap  12751  nonsq  12778  hashdvds  12792  prmdiv  12806  odzdvds  12817  pythagtriplem4  12840  pcpre1  12864  pcdvdsb  12892  pcz  12904  pcprmpw2  12905  pcaddlem  12911  pcadd  12912  pcadd2  12913  pcmpt  12915  pcmptdvds  12917  fldivp1  12920  pcfaclem  12921  pockthlem  12928  4sqlem6  12955  4sqlem8  12957  4sqexercise1  12970  4sqexercise2  12971  4sqlemsdc  12972  4sqlem11  12973  4sqlem12  12974  4sqlem14  12976  4sqlem16  12978  ennnfonelemkh  13032  nninfdclemp1  13070  eqgen  13813  dvdsrmul1  14115  unitmulclb  14127  subrguss  14249  znidom  14670  znunit  14672  mplsubgfilemcl  14712  psmetxrge0  15055  isxmet2d  15071  mettri  15096  xmettri3  15097  mettri3  15098  xblss2ps  15127  blss2ps  15129  blss2  15130  blssps  15150  blss  15151  xmetxp  15230  ivthdec  15367  ivthreinc  15368  hoverb  15371  hovergt0  15373  sin0pilem1  15504  sinq12gt0  15553  tangtx  15561  cosordlem  15572  cosq34lt1  15573  logdivlti  15604  logbgcd1irrap  15693  perfectlem1  15722  lgsdilem2  15764  gausslemma2dlem1f1o  15788  lgsquadlem1  15805  2lgsoddprmlem2  15834  2sqlem3  15845  2sqlem8  15851  usgrsizedgen  16063  cvgcmp2nlemabs  16636  trilpolemclim  16640  trilpolemeq1  16644  apdifflemf  16650  apdifflemr  16651  nconstwlpolemgt0  16668