Theorem breqtrrd 4137

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

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4109

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110

This theorem is referenced by:  frirrg  4471  fidcen  7156  unsnfidcex  7180  unsnfidcel  7181  addlocprlemeq  7848  ltexprlemopl  7916  recexprlemloc  7946  cauappcvgprlemopl  7961  cauappcvgprlemladdfu  7969  cauappcvgprlem1  7974  caucvgprlemopl  7984  caucvgprlemladdfu  7992  caucvgprprlemopl  8012  caucvgprprlemexbt  8021  mulgt0sr  8093  archsr  8097  caucvgsrlemoffgt1  8114  suplocsrlemb  8121  suplocsrlem  8123  mulap0r  8889  prodgt0  9126  div4p1lem1div2  9492  mul2lt0rgt0  10093  xnn0dcle  10135  xnn0letri  10136  xleadd1a  10206  xltadd1  10209  xlt2add  10213  xposdif  10215  xlesubadd  10216  xleaddadd  10220  uzsubsubfz  10381  fzctr  10467  subfzo0  10588  exbtwnzlemstep  10607  exbtwnzlemex  10609  rebtwn2zlemstep  10612  rebtwn2z  10614  qbtwnxr  10617  xqltnle  10627  fldiv4lem1div2uz2  10666  ceilqge  10672  modqge0  10694  modqlt  10695  modqid  10711  m1modge3gt1  10733  modaddmodup  10749  addmodlteq  10760  ser3mono  10849  seqf1oglem1  10881  seqf1oglem2  10882  ser3ge0  10898  ser3le  10899  leexp1a  10956  sqgt0ap  10970  sqge0  10978  nnlesq  11005  expnbnd  11025  nn0opthlem2d  11083  facwordi  11102  bcm1n  11131  filtinf  11154  hashunlem  11168  zfz1isolemiso  11211  cats1fvd  11458  cjmulge0  11574  resqrexlemover  11695  resqrexlemdec  11696  resqrexlemlo  11698  resqrexlemcalc3  11701  resqrexlemcvg  11704  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemga  11708  absge0  11745  amgm2  11803  maxle1  11896  bdtrilem  11924  xrmaxifle  11931  xrmaxiflemlub  11933  xrmaxiflemval  11935  xrmax1sup  11938  xrmaxltsup  11943  xrmaxadd  11946  xrbdtri  11961  reccn2ap  11998  climle  12019  climserle  12030  isumclim2  12108  isumclim3  12109  isumge0  12116  fsumlessfi  12146  expcnvap0  12188  expcnvre  12189  explecnv  12191  absltap  12195  cvgratnnlembern  12209  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratnnlemabsle  12213  cvgratnnlemfm  12215  cvgratnnlemrate  12216  mertenslemi1  12221  mertenslem2  12222  clim2divap  12226  prodmodclem3  12261  efcvg  12352  ege2le3  12357  efaddlem  12360  eftlub  12376  effsumlt  12378  ef01bndlem  12442  sin02gt0  12450  eirrap  12464  iddvdsexp  12501  dvdsadd  12522  dvdsfac  12546  dvdsmod  12548  3dvds  12550  omoe  12582  divalglemnn  12604  divalglemnqt  12606  flodddiv4t2lthalf  12625  bitsfzo  12641  bitsmod  12642  bitscmp  12644  bitsinv1lem  12647  dvdslegcd  12660  dfgcd3  12706  dvdssqim  12720  dvdsmulgcd  12721  nn0seqcvgd  12738  dvdslcm  12766  lcmgcdlem  12774  mulgcddvds  12791  qredeq  12793  cncongr2  12801  sqnprm  12833  isprm6  12844  sqpweven  12872  znege1  12875  sqrt2irrap  12877  nonsq  12904  hashdvds  12918  prmdiv  12932  odzdvds  12943  pythagtriplem4  12966  pcpre1  12990  pcdvdsb  13018  pcz  13030  pcprmpw2  13031  pcaddlem  13037  pcadd  13038  pcadd2  13039  pcmpt  13041  pcmptdvds  13043  fldivp1  13046  pcfaclem  13047  pockthlem  13054  4sqlem6  13081  4sqlem8  13083  4sqexercise1  13096  4sqexercise2  13097  4sqlemsdc  13098  4sqlem11  13099  4sqlem12  13100  4sqlem14  13102  4sqlem16  13104  ennnfonelemkh  13163  nninfdclemp1  13201  eqgen  13944  dvdsrmul1  14247  unitmulclb  14259  subrguss  14381  znidom  14805  znunit  14807  mplsubgfilemcl  14854  psmetxrge0  15197  isxmet2d  15213  mettri  15238  xmettri3  15239  mettri3  15240  xblss2ps  15269  blss2ps  15271  blss2  15272  blssps  15292  blss  15293  xmetxp  15372  ivthdec  15509  ivthreinc  15510  hoverb  15513  hovergt0  15515  sin0pilem1  15646  sinq12gt0  15695  tangtx  15703  cosordlem  15714  cosq34lt1  15715  logdivlti  15746  logbgcd1irrap  15835  perfectlem1  15867  lgsdilem2  15909  gausslemma2dlem1f1o  15933  lgsquadlem1  15950  2lgsoddprmlem2  15979  2sqlem3  15990  2sqlem8  15996  usgrsizedgen  16208  cvgcmp2nlemabs  16816  trilpolemclim  16820  trilpolemeq1  16824  apdifflemf  16830  apdifflemr  16831  nconstwlpolemgt0  16850