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  15882  sinq12gt0  15931  tangtx  15939  cosordlem  15950  cosq34lt1  15951  logdivlti  15982  logbgcd1irrap  16072  birthdaylem3  16089  perfectlem1  16113  lgsdilem2  16155  gausslemma2dlem1f1o  16179  lgsquadlem1  16196  2lgsoddprmlem2  16225  2sqlem3  16236  2sqlem8  16242  usgrsizedgen  16454  cvgcmp2nlemabs  17081  trilpolemclim  17085  trilpolemeq1  17089  apdifflemf  17095  apdifflemr  17096  nconstwlpolemgt0  17114