Theorem breqtrrd 4158

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 4156	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1402   class class class wbr 4130

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  frirrg  4495  fidcen  7203  unsnfidcex  7227  unsnfidcel  7228  addlocprlemeq  7900  ltexprlemopl  7968  recexprlemloc  7998  cauappcvgprlemopl  8013  cauappcvgprlemladdfu  8021  cauappcvgprlem1  8026  caucvgprlemopl  8036  caucvgprlemladdfu  8044  caucvgprprlemopl  8064  caucvgprprlemexbt  8073  mulgt0sr  8145  archsr  8149  caucvgsrlemoffgt1  8166  suplocsrlemb  8173  suplocsrlem  8175  mulap0r  8943  prodgt0  9182  div4p1lem1div2  9559  mul2lt0rgt0  10161  xnn0dcle  10204  xnn0letri  10205  xleadd1a  10275  xltadd1  10278  xlt2add  10282  xposdif  10284  xlesubadd  10285  xleaddadd  10289  uzsubsubfz  10452  fzctr  10540  subfzo0  10661  exbtwnzlemstep  10682  exbtwnzlemex  10684  rebtwn2zlemstep  10687  rebtwn2z  10689  qbtwnxr  10692  xqltnle  10702  fldiv4lem1div2uz2  10741  ceilqge  10747  modqge0  10769  modqlt  10770  modqid  10786  m1modge3gt1  10808  modaddmodup  10824  addmodlteq  10835  ser3mono  10924  seqf1oglem1  10956  seqf1oglem2  10957  ser3ge0  10973  ser3le  10974  leexp1a  11031  sqgt0ap  11045  sqge0  11053  nnlesq  11080  expnbnd  11101  nn0opthlem2d  11159  facwordi  11178  bcm1n  11207  filtinf  11230  hashunlem  11244  zfz1isolemiso  11291  cats1fvd  11538  cjmulge0  11654  resqrexlemover  11776  resqrexlemdec  11777  resqrexlemlo  11779  resqrexlemcalc3  11782  resqrexlemcvg  11785  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemga  11789  absge0  11826  amgm2  11884  maxle1  11977  bdtrilem  12005  xrmaxifle  12012  xrmaxiflemlub  12014  xrmaxiflemval  12016  xrmax1sup  12019  xrmaxltsup  12024  xrmaxadd  12027  xrbdtri  12042  reccn2ap  12079  climle  12100  climserle  12111  isumclim2  12189  isumclim3  12190  isumge0  12197  fsumlessfi  12227  expcnvap0  12269  expcnvre  12270  explecnv  12272  absltap  12276  cvgratnnlembern  12290  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratnnlemabsle  12294  cvgratnnlemfm  12296  cvgratnnlemrate  12297  mertenslemi1  12302  mertenslem2  12303  clim2divap  12307  prodmodclem3  12342  efcvg  12433  ege2le3  12438  efaddlem  12441  eftlub  12457  effsumlt  12459  ef01bndlem  12523  sin02gt0  12531  eirrap  12545  iddvdsexp  12582  dvdsadd  12603  dvdsfac  12627  dvdsmod  12629  3dvds  12631  omoe  12663  divalglemnn  12685  divalglemnqt  12687  flodddiv4t2lthalf  12706  bitsfzo  12722  bitsmod  12723  bitscmp  12725  bitsinv1lem  12728  dvdslegcd  12741  dfgcd3  12787  dvdssqim  12801  dvdsmulgcd  12802  nn0seqcvgd  12819  dvdslcm  12847  lcmgcdlem  12855  mulgcddvds  12872  qredeq  12874  cncongr2  12882  sqnprm  12914  isprm6  12925  sqpweven  12953  znege1  12956  sqrt2irrap  12958  nonsq  12985  hashdvds  12999  prmdiv  13013  odzdvds  13024  pythagtriplem4  13047  pcpre1  13071  pcdvdsb  13099  pcz  13111  pcprmpw2  13112  pcaddlem  13118  pcadd  13119  pcadd2  13120  pcmpt  13122  pcmptdvds  13124  fldivp1  13127  pcfaclem  13128  pockthlem  13135  4sqlem6  13162  4sqlem8  13164  4sqexercise1  13177  4sqexercise2  13178  4sqlemsdc  13179  4sqlem11  13180  4sqlem12  13181  4sqlem14  13183  4sqlem16  13185  ballotfilemsgt1  13254  ballotfilemsel1i  13256  ennnfonelemkh  13303  nninfdclemp1  13341  eqgen  14030  dvdsrmul1  14409  unitmulclb  14421  subrguss  14544  znidom  14992  znunit  14994  mplsubgfilemcl  15090  psmetxrge0  15433  isxmet2d  15449  mettri  15474  xmettri3  15475  mettri3  15476  xblss2ps  15505  blss2ps  15507  blss2  15508  blssps  15528  blss  15529  xmetxp  15608  ivthdec  15745  ivthreinc  15746  hoverb  15749  hovergt0  15751  sin0pilem1  15883  sinq12gt0  15932  tangtx  15940  cosordlem  15951  cosq34lt1  15952  logdivlti  15984  logbgcd1irrap  16076  birthdaylem3  16093  perfectlem1  16117  lgsdilem2  16159  gausslemma2dlem1f1o  16183  lgsquadlem1  16200  2lgsoddprmlem2  16229  2sqlem3  16240  2sqlem8  16246  usgrsizedgen  16458  cvgcmp2nlemabs  17085  trilpolemclim  17089  trilpolemeq1  17093  apdifflemf  17099  apdifflemr  17100  nconstwlpolemgt0  17118