Theorem breqtrrd 4153

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

Syntax hints:   → wi 4   = wceq 1402   class class class wbr 4125

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-br 4126

This theorem is referenced by:  frirrg  4490  fidcen  7193  unsnfidcex  7217  unsnfidcel  7218  addlocprlemeq  7890  ltexprlemopl  7958  recexprlemloc  7988  cauappcvgprlemopl  8003  cauappcvgprlemladdfu  8011  cauappcvgprlem1  8016  caucvgprlemopl  8026  caucvgprlemladdfu  8034  caucvgprprlemopl  8054  caucvgprprlemexbt  8063  mulgt0sr  8135  archsr  8139  caucvgsrlemoffgt1  8156  suplocsrlemb  8163  suplocsrlem  8165  mulap0r  8933  prodgt0  9172  div4p1lem1div2  9538  mul2lt0rgt0  10140  xnn0dcle  10183  xnn0letri  10184  xleadd1a  10254  xltadd1  10257  xlt2add  10261  xposdif  10263  xlesubadd  10264  xleaddadd  10268  uzsubsubfz  10430  fzctr  10518  subfzo0  10639  exbtwnzlemstep  10660  exbtwnzlemex  10662  rebtwn2zlemstep  10665  rebtwn2z  10667  qbtwnxr  10670  xqltnle  10680  fldiv4lem1div2uz2  10719  ceilqge  10725  modqge0  10747  modqlt  10748  modqid  10764  m1modge3gt1  10786  modaddmodup  10802  addmodlteq  10813  ser3mono  10902  seqf1oglem1  10934  seqf1oglem2  10935  ser3ge0  10951  ser3le  10952  leexp1a  11009  sqgt0ap  11023  sqge0  11031  nnlesq  11058  expnbnd  11079  nn0opthlem2d  11137  facwordi  11156  bcm1n  11185  filtinf  11208  hashunlem  11222  zfz1isolemiso  11269  cats1fvd  11516  cjmulge0  11632  resqrexlemover  11754  resqrexlemdec  11755  resqrexlemlo  11757  resqrexlemcalc3  11760  resqrexlemcvg  11763  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemga  11767  absge0  11804  amgm2  11862  maxle1  11955  bdtrilem  11983  xrmaxifle  11990  xrmaxiflemlub  11992  xrmaxiflemval  11994  xrmax1sup  11997  xrmaxltsup  12002  xrmaxadd  12005  xrbdtri  12020  reccn2ap  12057  climle  12078  climserle  12089  isumclim2  12167  isumclim3  12168  isumge0  12175  fsumlessfi  12205  expcnvap0  12247  expcnvre  12248  explecnv  12250  absltap  12254  cvgratnnlembern  12268  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratnnlemabsle  12272  cvgratnnlemfm  12274  cvgratnnlemrate  12275  mertenslemi1  12280  mertenslem2  12281  clim2divap  12285  prodmodclem3  12320  efcvg  12411  ege2le3  12416  efaddlem  12419  eftlub  12435  effsumlt  12437  ef01bndlem  12501  sin02gt0  12509  eirrap  12523  iddvdsexp  12560  dvdsadd  12581  dvdsfac  12605  dvdsmod  12607  3dvds  12609  omoe  12641  divalglemnn  12663  divalglemnqt  12665  flodddiv4t2lthalf  12684  bitsfzo  12700  bitsmod  12701  bitscmp  12703  bitsinv1lem  12706  dvdslegcd  12719  dfgcd3  12765  dvdssqim  12779  dvdsmulgcd  12780  nn0seqcvgd  12797  dvdslcm  12825  lcmgcdlem  12833  mulgcddvds  12850  qredeq  12852  cncongr2  12860  sqnprm  12892  isprm6  12903  sqpweven  12931  znege1  12934  sqrt2irrap  12936  nonsq  12963  hashdvds  12977  prmdiv  12991  odzdvds  13002  pythagtriplem4  13025  pcpre1  13049  pcdvdsb  13077  pcz  13089  pcprmpw2  13090  pcaddlem  13096  pcadd  13097  pcadd2  13098  pcmpt  13100  pcmptdvds  13102  fldivp1  13105  pcfaclem  13106  pockthlem  13113  4sqlem6  13140  4sqlem8  13142  4sqexercise1  13155  4sqexercise2  13156  4sqlemsdc  13157  4sqlem11  13158  4sqlem12  13159  4sqlem14  13161  4sqlem16  13163  ballotfilemsgt1  13232  ballotfilemsel1i  13234  ennnfonelemkh  13281  nninfdclemp1  13319  eqgen  14007  dvdsrmul1  14382  unitmulclb  14394  subrguss  14517  znidom  14964  znunit  14966  mplsubgfilemcl  15013  psmetxrge0  15356  isxmet2d  15372  mettri  15397  xmettri3  15398  mettri3  15399  xblss2ps  15428  blss2ps  15430  blss2  15431  blssps  15451  blss  15452  xmetxp  15531  ivthdec  15668  ivthreinc  15669  hoverb  15672  hovergt0  15674  sin0pilem1  15805  sinq12gt0  15854  tangtx  15862  cosordlem  15873  cosq34lt1  15874  logdivlti  15905  logbgcd1irrap  15995  perfectlem1  16027  lgsdilem2  16069  gausslemma2dlem1f1o  16093  lgsquadlem1  16110  2lgsoddprmlem2  16139  2sqlem3  16150  2sqlem8  16156  usgrsizedgen  16368  cvgcmp2nlemabs  16986  trilpolemclim  16990  trilpolemeq1  16994  apdifflemf  17000  apdifflemr  17001  nconstwlpolemgt0  17019