Theorem breqtrrd 4062

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

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4034

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  frirrg  4386  unsnfidcex  6990  unsnfidcel  6991  addlocprlemeq  7619  ltexprlemopl  7687  recexprlemloc  7717  cauappcvgprlemopl  7732  cauappcvgprlemladdfu  7740  cauappcvgprlem1  7745  caucvgprlemopl  7755  caucvgprlemladdfu  7763  caucvgprprlemopl  7783  caucvgprprlemexbt  7792  mulgt0sr  7864  archsr  7868  caucvgsrlemoffgt1  7885  suplocsrlemb  7892  suplocsrlem  7894  mulap0r  8661  prodgt0  8898  div4p1lem1div2  9264  mul2lt0rgt0  9854  xnn0dcle  9896  xnn0letri  9897  xleadd1a  9967  xltadd1  9970  xlt2add  9974  xposdif  9976  xlesubadd  9977  xleaddadd  9981  uzsubsubfz  10141  fzctr  10227  subfzo0  10337  exbtwnzlemstep  10356  exbtwnzlemex  10358  rebtwn2zlemstep  10361  rebtwn2z  10363  qbtwnxr  10366  xqltnle  10376  fldiv4lem1div2uz2  10415  ceilqge  10421  modqge0  10443  modqlt  10444  modqid  10460  m1modge3gt1  10482  modaddmodup  10498  addmodlteq  10509  ser3mono  10598  seqf1oglem1  10630  seqf1oglem2  10631  ser3ge0  10647  ser3le  10648  leexp1a  10705  sqgt0ap  10719  sqge0  10727  nnlesq  10754  expnbnd  10774  nn0opthlem2d  10832  facwordi  10851  filtinf  10902  hashunlem  10915  zfz1isolemiso  10950  cjmulge0  11073  resqrexlemover  11194  resqrexlemdec  11195  resqrexlemlo  11197  resqrexlemcalc3  11200  resqrexlemcvg  11203  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemga  11207  absge0  11244  amgm2  11302  maxle1  11395  bdtrilem  11423  xrmaxifle  11430  xrmaxiflemlub  11432  xrmaxiflemval  11434  xrmax1sup  11437  xrmaxltsup  11442  xrmaxadd  11445  xrbdtri  11460  reccn2ap  11497  climle  11518  climserle  11529  isumclim2  11606  isumclim3  11607  isumge0  11614  fsumlessfi  11644  expcnvap0  11686  expcnvre  11687  explecnv  11689  absltap  11693  cvgratnnlembern  11707  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratnnlemabsle  11711  cvgratnnlemfm  11713  cvgratnnlemrate  11714  mertenslemi1  11719  mertenslem2  11720  clim2divap  11724  prodmodclem3  11759  efcvg  11850  ege2le3  11855  efaddlem  11858  eftlub  11874  effsumlt  11876  ef01bndlem  11940  sin02gt0  11948  eirrap  11962  iddvdsexp  11999  dvdsadd  12020  dvdsfac  12044  dvdsmod  12046  3dvds  12048  omoe  12080  divalglemnn  12102  divalglemnqt  12104  flodddiv4t2lthalf  12123  bitsfzo  12139  bitsmod  12140  bitscmp  12142  bitsinv1lem  12145  dvdslegcd  12158  dfgcd3  12204  dvdssqim  12218  dvdsmulgcd  12219  nn0seqcvgd  12236  dvdslcm  12264  lcmgcdlem  12272  mulgcddvds  12289  qredeq  12291  cncongr2  12299  sqnprm  12331  isprm6  12342  sqpweven  12370  znege1  12373  sqrt2irrap  12375  nonsq  12402  hashdvds  12416  prmdiv  12430  odzdvds  12441  pythagtriplem4  12464  pcpre1  12488  pcdvdsb  12516  pcz  12528  pcprmpw2  12529  pcaddlem  12535  pcadd  12536  pcadd2  12537  pcmpt  12539  pcmptdvds  12541  fldivp1  12544  pcfaclem  12545  pockthlem  12552  4sqlem6  12579  4sqlem8  12581  4sqexercise1  12594  4sqexercise2  12595  4sqlemsdc  12596  4sqlem11  12597  4sqlem12  12598  4sqlem14  12600  4sqlem16  12602  ennnfonelemkh  12656  nninfdclemp1  12694  eqgen  13435  dvdsrmul1  13736  unitmulclb  13748  subrguss  13870  znidom  14291  znunit  14293  mplsubgfilemcl  14333  psmetxrge0  14676  isxmet2d  14692  mettri  14717  xmettri3  14718  mettri3  14719  xblss2ps  14748  blss2ps  14750  blss2  14751  blssps  14771  blss  14772  xmetxp  14851  ivthdec  14988  ivthreinc  14989  hoverb  14992  hovergt0  14994  sin0pilem1  15125  sinq12gt0  15174  tangtx  15182  cosordlem  15193  cosq34lt1  15194  logdivlti  15225  logbgcd1irrap  15314  perfectlem1  15343  lgsdilem2  15385  gausslemma2dlem1f1o  15409  lgsquadlem1  15426  2lgsoddprmlem2  15455  2sqlem3  15466  2sqlem8  15472  cvgcmp2nlemabs  15789  trilpolemclim  15793  trilpolemeq1  15797  apdifflemf  15803  apdifflemr  15804  nconstwlpolemgt0  15821