Theorem breqtrrd 4010

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

Syntax hints:   → wi 4   = wceq 1343   class class class wbr 3982

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-br 3983

This theorem is referenced by:  frirrg  4328  unsnfidcex  6885  unsnfidcel  6886  addlocprlemeq  7474  ltexprlemopl  7542  recexprlemloc  7572  cauappcvgprlemopl  7587  cauappcvgprlemladdfu  7595  cauappcvgprlem1  7600  caucvgprlemopl  7610  caucvgprlemladdfu  7618  caucvgprprlemopl  7638  caucvgprprlemexbt  7647  mulgt0sr  7719  archsr  7723  caucvgsrlemoffgt1  7740  suplocsrlemb  7747  suplocsrlem  7749  mulap0r  8513  prodgt0  8747  div4p1lem1div2  9110  mul2lt0rgt0  9696  xnn0dcle  9738  xnn0letri  9739  xleadd1a  9809  xltadd1  9812  xlt2add  9816  xposdif  9818  xlesubadd  9819  xleaddadd  9823  uzsubsubfz  9982  fzctr  10068  subfzo0  10177  exbtwnzlemstep  10183  exbtwnzlemex  10185  rebtwn2zlemstep  10188  rebtwn2z  10190  qbtwnxr  10193  ceilqge  10245  modqge0  10267  modqlt  10268  modqid  10284  m1modge3gt1  10306  modaddmodup  10322  addmodlteq  10333  ser3mono  10413  ser3ge0  10452  ser3le  10453  leexp1a  10510  sqgt0ap  10523  sqge0  10531  nnlesq  10558  expnbnd  10578  nn0opthlem2d  10634  facwordi  10653  filtinf  10705  hashunlem  10717  zfz1isolemiso  10752  cjmulge0  10831  resqrexlemover  10952  resqrexlemdec  10953  resqrexlemlo  10955  resqrexlemcalc3  10958  resqrexlemcvg  10961  resqrexlemoverl  10963  resqrexlemglsq  10964  resqrexlemga  10965  absge0  11002  amgm2  11060  maxle1  11153  bdtrilem  11180  xrmaxifle  11187  xrmaxiflemlub  11189  xrmaxiflemval  11191  xrmax1sup  11194  xrmaxltsup  11199  xrmaxadd  11202  xrbdtri  11217  reccn2ap  11254  climle  11275  climserle  11286  isumclim2  11363  isumclim3  11364  isumge0  11371  fsumlessfi  11401  expcnvap0  11443  expcnvre  11444  explecnv  11446  absltap  11450  cvgratnnlembern  11464  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratnnlemabsle  11468  cvgratnnlemfm  11470  cvgratnnlemrate  11471  mertenslemi1  11476  mertenslem2  11477  clim2divap  11481  prodmodclem3  11516  efcvg  11607  ege2le3  11612  efaddlem  11615  eftlub  11631  effsumlt  11633  ef01bndlem  11697  sin02gt0  11704  eirrap  11718  iddvdsexp  11755  dvdsadd  11776  dvdsfac  11798  dvdsmod  11800  omoe  11833  divalglemnn  11855  divalglemnqt  11857  flodddiv4t2lthalf  11874  dvdslegcd  11897  dfgcd3  11943  dvdssqim  11957  dvdsmulgcd  11958  nn0seqcvgd  11973  dvdslcm  12001  lcmgcdlem  12009  mulgcddvds  12026  qredeq  12028  cncongr2  12036  sqnprm  12068  isprm6  12079  sqpweven  12107  znege1  12110  sqrt2irrap  12112  nonsq  12139  hashdvds  12153  prmdiv  12167  odzdvds  12177  pythagtriplem4  12200  pcpre1  12224  pcdvdsb  12251  pcz  12263  pcprmpw2  12264  pcaddlem  12270  pcadd  12271  pcmpt  12273  pcmptdvds  12275  fldivp1  12278  pcfaclem  12279  pockthlem  12286  4sqlem6  12313  4sqlem8  12315  ennnfonelemkh  12345  nninfdclemp1  12383  psmetxrge0  12972  isxmet2d  12988  mettri  13013  xmettri3  13014  mettri3  13015  xblss2ps  13044  blss2ps  13046  blss2  13047  blssps  13067  blss  13068  xmetxp  13147  ivthdec  13262  sin0pilem1  13342  sinq12gt0  13391  tangtx  13399  cosordlem  13410  cosq34lt1  13411  logdivlti  13442  logbgcd1irrap  13528  lgsdilem2  13577  2sqlem3  13593  2sqlem8  13599  cvgcmp2nlemabs  13911  trilpolemclim  13915  trilpolemeq1  13919  apdifflemf  13925  apdifflemr  13926  nconstwlpolemgt0  13942