Theorem breqtrrd 4073

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

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4045

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046

This theorem is referenced by:  frirrg  4398  unsnfidcex  7019  unsnfidcel  7020  addlocprlemeq  7648  ltexprlemopl  7716  recexprlemloc  7746  cauappcvgprlemopl  7761  cauappcvgprlemladdfu  7769  cauappcvgprlem1  7774  caucvgprlemopl  7784  caucvgprlemladdfu  7792  caucvgprprlemopl  7812  caucvgprprlemexbt  7821  mulgt0sr  7893  archsr  7897  caucvgsrlemoffgt1  7914  suplocsrlemb  7921  suplocsrlem  7923  mulap0r  8690  prodgt0  8927  div4p1lem1div2  9293  mul2lt0rgt0  9884  xnn0dcle  9926  xnn0letri  9927  xleadd1a  9997  xltadd1  10000  xlt2add  10004  xposdif  10006  xlesubadd  10007  xleaddadd  10011  uzsubsubfz  10171  fzctr  10257  subfzo0  10373  exbtwnzlemstep  10392  exbtwnzlemex  10394  rebtwn2zlemstep  10397  rebtwn2z  10399  qbtwnxr  10402  xqltnle  10412  fldiv4lem1div2uz2  10451  ceilqge  10457  modqge0  10479  modqlt  10480  modqid  10496  m1modge3gt1  10518  modaddmodup  10534  addmodlteq  10545  ser3mono  10634  seqf1oglem1  10666  seqf1oglem2  10667  ser3ge0  10683  ser3le  10684  leexp1a  10741  sqgt0ap  10755  sqge0  10763  nnlesq  10790  expnbnd  10810  nn0opthlem2d  10868  facwordi  10887  filtinf  10938  hashunlem  10951  zfz1isolemiso  10986  cjmulge0  11233  resqrexlemover  11354  resqrexlemdec  11355  resqrexlemlo  11357  resqrexlemcalc3  11360  resqrexlemcvg  11363  resqrexlemoverl  11365  resqrexlemglsq  11366  resqrexlemga  11367  absge0  11404  amgm2  11462  maxle1  11555  bdtrilem  11583  xrmaxifle  11590  xrmaxiflemlub  11592  xrmaxiflemval  11594  xrmax1sup  11597  xrmaxltsup  11602  xrmaxadd  11605  xrbdtri  11620  reccn2ap  11657  climle  11678  climserle  11689  isumclim2  11766  isumclim3  11767  isumge0  11774  fsumlessfi  11804  expcnvap0  11846  expcnvre  11847  explecnv  11849  absltap  11853  cvgratnnlembern  11867  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  cvgratnnlemabsle  11871  cvgratnnlemfm  11873  cvgratnnlemrate  11874  mertenslemi1  11879  mertenslem2  11880  clim2divap  11884  prodmodclem3  11919  efcvg  12010  ege2le3  12015  efaddlem  12018  eftlub  12034  effsumlt  12036  ef01bndlem  12100  sin02gt0  12108  eirrap  12122  iddvdsexp  12159  dvdsadd  12180  dvdsfac  12204  dvdsmod  12206  3dvds  12208  omoe  12240  divalglemnn  12262  divalglemnqt  12264  flodddiv4t2lthalf  12283  bitsfzo  12299  bitsmod  12300  bitscmp  12302  bitsinv1lem  12305  dvdslegcd  12318  dfgcd3  12364  dvdssqim  12378  dvdsmulgcd  12379  nn0seqcvgd  12396  dvdslcm  12424  lcmgcdlem  12432  mulgcddvds  12449  qredeq  12451  cncongr2  12459  sqnprm  12491  isprm6  12502  sqpweven  12530  znege1  12533  sqrt2irrap  12535  nonsq  12562  hashdvds  12576  prmdiv  12590  odzdvds  12601  pythagtriplem4  12624  pcpre1  12648  pcdvdsb  12676  pcz  12688  pcprmpw2  12689  pcaddlem  12695  pcadd  12696  pcadd2  12697  pcmpt  12699  pcmptdvds  12701  fldivp1  12704  pcfaclem  12705  pockthlem  12712  4sqlem6  12739  4sqlem8  12741  4sqexercise1  12754  4sqexercise2  12755  4sqlemsdc  12756  4sqlem11  12757  4sqlem12  12758  4sqlem14  12760  4sqlem16  12762  ennnfonelemkh  12816  nninfdclemp1  12854  eqgen  13596  dvdsrmul1  13897  unitmulclb  13909  subrguss  14031  znidom  14452  znunit  14454  mplsubgfilemcl  14494  psmetxrge0  14837  isxmet2d  14853  mettri  14878  xmettri3  14879  mettri3  14880  xblss2ps  14909  blss2ps  14911  blss2  14912  blssps  14932  blss  14933  xmetxp  15012  ivthdec  15149  ivthreinc  15150  hoverb  15153  hovergt0  15155  sin0pilem1  15286  sinq12gt0  15335  tangtx  15343  cosordlem  15354  cosq34lt1  15355  logdivlti  15386  logbgcd1irrap  15475  perfectlem1  15504  lgsdilem2  15546  gausslemma2dlem1f1o  15570  lgsquadlem1  15587  2lgsoddprmlem2  15616  2sqlem3  15627  2sqlem8  15633  cvgcmp2nlemabs  16008  trilpolemclim  16012  trilpolemeq1  16016  apdifflemf  16022  apdifflemr  16023  nconstwlpolemgt0  16040