Theorem breqtrrd 4057

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

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4029

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  frirrg  4381  unsnfidcex  6976  unsnfidcel  6977  addlocprlemeq  7593  ltexprlemopl  7661  recexprlemloc  7691  cauappcvgprlemopl  7706  cauappcvgprlemladdfu  7714  cauappcvgprlem1  7719  caucvgprlemopl  7729  caucvgprlemladdfu  7737  caucvgprprlemopl  7757  caucvgprprlemexbt  7766  mulgt0sr  7838  archsr  7842  caucvgsrlemoffgt1  7859  suplocsrlemb  7866  suplocsrlem  7868  mulap0r  8634  prodgt0  8871  div4p1lem1div2  9236  mul2lt0rgt0  9826  xnn0dcle  9868  xnn0letri  9869  xleadd1a  9939  xltadd1  9942  xlt2add  9946  xposdif  9948  xlesubadd  9949  xleaddadd  9953  uzsubsubfz  10113  fzctr  10199  subfzo0  10309  exbtwnzlemstep  10316  exbtwnzlemex  10318  rebtwn2zlemstep  10321  rebtwn2z  10323  qbtwnxr  10326  xqltnle  10336  fldiv4lem1div2uz2  10375  ceilqge  10381  modqge0  10403  modqlt  10404  modqid  10420  m1modge3gt1  10442  modaddmodup  10458  addmodlteq  10469  ser3mono  10558  seqf1oglem1  10590  seqf1oglem2  10591  ser3ge0  10607  ser3le  10608  leexp1a  10665  sqgt0ap  10679  sqge0  10687  nnlesq  10714  expnbnd  10734  nn0opthlem2d  10792  facwordi  10811  filtinf  10862  hashunlem  10875  zfz1isolemiso  10910  cjmulge0  11033  resqrexlemover  11154  resqrexlemdec  11155  resqrexlemlo  11157  resqrexlemcalc3  11160  resqrexlemcvg  11163  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemga  11167  absge0  11204  amgm2  11262  maxle1  11355  bdtrilem  11382  xrmaxifle  11389  xrmaxiflemlub  11391  xrmaxiflemval  11393  xrmax1sup  11396  xrmaxltsup  11401  xrmaxadd  11404  xrbdtri  11419  reccn2ap  11456  climle  11477  climserle  11488  isumclim2  11565  isumclim3  11566  isumge0  11573  fsumlessfi  11603  expcnvap0  11645  expcnvre  11646  explecnv  11648  absltap  11652  cvgratnnlembern  11666  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemabsle  11670  cvgratnnlemfm  11672  cvgratnnlemrate  11673  mertenslemi1  11678  mertenslem2  11679  clim2divap  11683  prodmodclem3  11718  efcvg  11809  ege2le3  11814  efaddlem  11817  eftlub  11833  effsumlt  11835  ef01bndlem  11899  sin02gt0  11907  eirrap  11921  iddvdsexp  11958  dvdsadd  11979  dvdsfac  12002  dvdsmod  12004  omoe  12037  divalglemnn  12059  divalglemnqt  12061  flodddiv4t2lthalf  12078  dvdslegcd  12101  dfgcd3  12147  dvdssqim  12161  dvdsmulgcd  12162  nn0seqcvgd  12179  dvdslcm  12207  lcmgcdlem  12215  mulgcddvds  12232  qredeq  12234  cncongr2  12242  sqnprm  12274  isprm6  12285  sqpweven  12313  znege1  12316  sqrt2irrap  12318  nonsq  12345  hashdvds  12359  prmdiv  12373  odzdvds  12383  pythagtriplem4  12406  pcpre1  12430  pcdvdsb  12458  pcz  12470  pcprmpw2  12471  pcaddlem  12477  pcadd  12478  pcadd2  12479  pcmpt  12481  pcmptdvds  12483  fldivp1  12486  pcfaclem  12487  pockthlem  12494  4sqlem6  12521  4sqlem8  12523  4sqexercise1  12536  4sqexercise2  12537  4sqlemsdc  12538  4sqlem11  12539  4sqlem12  12540  4sqlem14  12542  4sqlem16  12544  ennnfonelemkh  12569  nninfdclemp1  12607  eqgen  13297  dvdsrmul1  13598  unitmulclb  13610  subrguss  13732  znidom  14145  znunit  14147  psmetxrge0  14500  isxmet2d  14516  mettri  14541  xmettri3  14542  mettri3  14543  xblss2ps  14572  blss2ps  14574  blss2  14575  blssps  14595  blss  14596  xmetxp  14675  ivthdec  14798  ivthreinc  14799  hoverb  14802  hovergt0  14804  sin0pilem1  14916  sinq12gt0  14965  tangtx  14973  cosordlem  14984  cosq34lt1  14985  logdivlti  15016  logbgcd1irrap  15102  lgsdilem2  15152  gausslemma2dlem1f1o  15176  lgsquadlem1  15191  2lgsoddprmlem2  15194  2sqlem3  15204  2sqlem8  15210  cvgcmp2nlemabs  15522  trilpolemclim  15526  trilpolemeq1  15530  apdifflemf  15536  apdifflemr  15537  nconstwlpolemgt0  15554