Theorem breqtrrd 4004

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

Syntax hints:   → wi 4   = wceq 1342   class class class wbr 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-br 3977

This theorem is referenced by:  frirrg  4322  unsnfidcex  6876  unsnfidcel  6877  addlocprlemeq  7465  ltexprlemopl  7533  recexprlemloc  7563  cauappcvgprlemopl  7578  cauappcvgprlemladdfu  7586  cauappcvgprlem1  7591  caucvgprlemopl  7601  caucvgprlemladdfu  7609  caucvgprprlemopl  7629  caucvgprprlemexbt  7638  mulgt0sr  7710  archsr  7714  caucvgsrlemoffgt1  7731  suplocsrlemb  7738  suplocsrlem  7740  mulap0r  8504  prodgt0  8738  div4p1lem1div2  9101  mul2lt0rgt0  9687  xnn0dcle  9729  xnn0letri  9730  xleadd1a  9800  xltadd1  9803  xlt2add  9807  xposdif  9809  xlesubadd  9810  xleaddadd  9814  uzsubsubfz  9972  fzctr  10058  subfzo0  10167  exbtwnzlemstep  10173  exbtwnzlemex  10175  rebtwn2zlemstep  10178  rebtwn2z  10180  qbtwnxr  10183  ceilqge  10235  modqge0  10257  modqlt  10258  modqid  10274  m1modge3gt1  10296  modaddmodup  10312  addmodlteq  10323  ser3mono  10403  ser3ge0  10442  ser3le  10443  leexp1a  10500  sqgt0ap  10513  sqge0  10521  nnlesq  10548  expnbnd  10567  nn0opthlem2d  10623  facwordi  10642  filtinf  10694  hashunlem  10706  zfz1isolemiso  10738  cjmulge0  10817  resqrexlemover  10938  resqrexlemdec  10939  resqrexlemlo  10941  resqrexlemcalc3  10944  resqrexlemcvg  10947  resqrexlemoverl  10949  resqrexlemglsq  10950  resqrexlemga  10951  absge0  10988  amgm2  11046  maxle1  11139  bdtrilem  11166  xrmaxifle  11173  xrmaxiflemlub  11175  xrmaxiflemval  11177  xrmax1sup  11180  xrmaxltsup  11185  xrmaxadd  11188  xrbdtri  11203  reccn2ap  11240  climle  11261  climserle  11272  isumclim2  11349  isumclim3  11350  isumge0  11357  fsumlessfi  11387  expcnvap0  11429  expcnvre  11430  explecnv  11432  absltap  11436  cvgratnnlembern  11450  cvgratnnlemnexp  11451  cvgratnnlemmn  11452  cvgratnnlemabsle  11454  cvgratnnlemfm  11456  cvgratnnlemrate  11457  mertenslemi1  11462  mertenslem2  11463  clim2divap  11467  prodmodclem3  11502  efcvg  11593  ege2le3  11598  efaddlem  11601  eftlub  11617  effsumlt  11619  ef01bndlem  11683  sin02gt0  11690  eirrap  11704  iddvdsexp  11741  dvdsadd  11761  dvdsfac  11783  dvdsmod  11785  omoe  11818  divalglemnn  11840  divalglemnqt  11842  flodddiv4t2lthalf  11859  dvdslegcd  11882  dfgcd3  11928  dvdssqim  11942  dvdsmulgcd  11943  nn0seqcvgd  11952  dvdslcm  11980  lcmgcdlem  11988  mulgcddvds  12005  qredeq  12007  cncongr2  12015  sqnprm  12047  isprm6  12056  sqpweven  12084  znege1  12087  sqrt2irrap  12089  nonsq  12116  hashdvds  12130  prmdiv  12144  odzdvds  12154  pythagtriplem4  12177  pcpre1  12201  pcdvdsb  12228  pcz  12240  pcprmpw2  12241  pcaddlem  12247  pcadd  12248  pcmpt  12250  pcmptdvds  12252  fldivp1  12255  pcfaclem  12256  ennnfonelemkh  12282  nninfdclemp1  12322  psmetxrge0  12873  isxmet2d  12889  mettri  12914  xmettri3  12915  mettri3  12916  xblss2ps  12945  blss2ps  12947  blss2  12948  blssps  12968  blss  12969  xmetxp  13048  ivthdec  13163  sin0pilem1  13243  sinq12gt0  13292  tangtx  13300  cosordlem  13311  cosq34lt1  13312  logdivlti  13343  logbgcd1irrap  13429  cvgcmp2nlemabs  13745  trilpolemclim  13749  trilpolemeq1  13753  apdifflemf  13759  apdifflemr  13760  nconstwlpolemgt0  13776