Theorem breqtrrd 4072

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 2211	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrd 4070	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 4045

This theorem is referenced by:  frirrg  4397  unsnfidcex  7017  unsnfidcel  7018  addlocprlemeq  7646  ltexprlemopl  7714  recexprlemloc  7744  cauappcvgprlemopl  7759  cauappcvgprlemladdfu  7767  cauappcvgprlem1  7772  caucvgprlemopl  7782  caucvgprlemladdfu  7790  caucvgprprlemopl  7810  caucvgprprlemexbt  7819  mulgt0sr  7891  archsr  7895  caucvgsrlemoffgt1  7912  suplocsrlemb  7919  suplocsrlem  7921  mulap0r  8688  prodgt0  8925  div4p1lem1div2  9291  mul2lt0rgt0  9882  xnn0dcle  9924  xnn0letri  9925  xleadd1a  9995  xltadd1  9998  xlt2add  10002  xposdif  10004  xlesubadd  10005  xleaddadd  10009  uzsubsubfz  10169  fzctr  10255  subfzo0  10371  exbtwnzlemstep  10390  exbtwnzlemex  10392  rebtwn2zlemstep  10395  rebtwn2z  10397  qbtwnxr  10400  xqltnle  10410  fldiv4lem1div2uz2  10449  ceilqge  10455  modqge0  10477  modqlt  10478  modqid  10494  m1modge3gt1  10516  modaddmodup  10532  addmodlteq  10543  ser3mono  10632  seqf1oglem1  10664  seqf1oglem2  10665  ser3ge0  10681  ser3le  10682  leexp1a  10739  sqgt0ap  10753  sqge0  10761  nnlesq  10788  expnbnd  10808  nn0opthlem2d  10866  facwordi  10885  filtinf  10936  hashunlem  10949  zfz1isolemiso  10984  cjmulge0  11200  resqrexlemover  11321  resqrexlemdec  11322  resqrexlemlo  11324  resqrexlemcalc3  11327  resqrexlemcvg  11330  resqrexlemoverl  11332  resqrexlemglsq  11333  resqrexlemga  11334  absge0  11371  amgm2  11429  maxle1  11522  bdtrilem  11550  xrmaxifle  11557  xrmaxiflemlub  11559  xrmaxiflemval  11561  xrmax1sup  11564  xrmaxltsup  11569  xrmaxadd  11572  xrbdtri  11587  reccn2ap  11624  climle  11645  climserle  11656  isumclim2  11733  isumclim3  11734  isumge0  11741  fsumlessfi  11771  expcnvap0  11813  expcnvre  11814  explecnv  11816  absltap  11820  cvgratnnlembern  11834  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  cvgratnnlemabsle  11838  cvgratnnlemfm  11840  cvgratnnlemrate  11841  mertenslemi1  11846  mertenslem2  11847  clim2divap  11851  prodmodclem3  11886  efcvg  11977  ege2le3  11982  efaddlem  11985  eftlub  12001  effsumlt  12003  ef01bndlem  12067  sin02gt0  12075  eirrap  12089  iddvdsexp  12126  dvdsadd  12147  dvdsfac  12171  dvdsmod  12173  3dvds  12175  omoe  12207  divalglemnn  12229  divalglemnqt  12231  flodddiv4t2lthalf  12250  bitsfzo  12266  bitsmod  12267  bitscmp  12269  bitsinv1lem  12272  dvdslegcd  12285  dfgcd3  12331  dvdssqim  12345  dvdsmulgcd  12346  nn0seqcvgd  12363  dvdslcm  12391  lcmgcdlem  12399  mulgcddvds  12416  qredeq  12418  cncongr2  12426  sqnprm  12458  isprm6  12469  sqpweven  12497  znege1  12500  sqrt2irrap  12502  nonsq  12529  hashdvds  12543  prmdiv  12557  odzdvds  12568  pythagtriplem4  12591  pcpre1  12615  pcdvdsb  12643  pcz  12655  pcprmpw2  12656  pcaddlem  12662  pcadd  12663  pcadd2  12664  pcmpt  12666  pcmptdvds  12668  fldivp1  12671  pcfaclem  12672  pockthlem  12679  4sqlem6  12706  4sqlem8  12708  4sqexercise1  12721  4sqexercise2  12722  4sqlemsdc  12723  4sqlem11  12724  4sqlem12  12725  4sqlem14  12727  4sqlem16  12729  ennnfonelemkh  12783  nninfdclemp1  12821  eqgen  13563  dvdsrmul1  13864  unitmulclb  13876  subrguss  13998  znidom  14419  znunit  14421  mplsubgfilemcl  14461  psmetxrge0  14804  isxmet2d  14820  mettri  14845  xmettri3  14846  mettri3  14847  xblss2ps  14876  blss2ps  14878  blss2  14879  blssps  14899  blss  14900  xmetxp  14979  ivthdec  15116  ivthreinc  15117  hoverb  15120  hovergt0  15122  sin0pilem1  15253  sinq12gt0  15302  tangtx  15310  cosordlem  15321  cosq34lt1  15322  logdivlti  15353  logbgcd1irrap  15442  perfectlem1  15471  lgsdilem2  15513  gausslemma2dlem1f1o  15537  lgsquadlem1  15554  2lgsoddprmlem2  15583  2sqlem3  15594  2sqlem8  15600  cvgcmp2nlemabs  15975  trilpolemclim  15979  trilpolemeq1  15983  apdifflemf  15989  apdifflemr  15990  nconstwlpolemgt0  16007