Theorem breqtrrd 4046

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

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

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 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-br 4019

This theorem is referenced by:  frirrg  4368  unsnfidcex  6949  unsnfidcel  6950  addlocprlemeq  7563  ltexprlemopl  7631  recexprlemloc  7661  cauappcvgprlemopl  7676  cauappcvgprlemladdfu  7684  cauappcvgprlem1  7689  caucvgprlemopl  7699  caucvgprlemladdfu  7707  caucvgprprlemopl  7727  caucvgprprlemexbt  7736  mulgt0sr  7808  archsr  7812  caucvgsrlemoffgt1  7829  suplocsrlemb  7836  suplocsrlem  7838  mulap0r  8603  prodgt0  8840  div4p1lem1div2  9203  mul2lt0rgt0  9792  xnn0dcle  9834  xnn0letri  9835  xleadd1a  9905  xltadd1  9908  xlt2add  9912  xposdif  9914  xlesubadd  9915  xleaddadd  9919  uzsubsubfz  10079  fzctr  10165  subfzo0  10274  exbtwnzlemstep  10280  exbtwnzlemex  10282  rebtwn2zlemstep  10285  rebtwn2z  10287  qbtwnxr  10290  xqltnle  10300  ceilqge  10343  modqge0  10365  modqlt  10366  modqid  10382  m1modge3gt1  10404  modaddmodup  10420  addmodlteq  10431  ser3mono  10511  ser3ge0  10551  ser3le  10552  leexp1a  10609  sqgt0ap  10623  sqge0  10631  nnlesq  10658  expnbnd  10678  nn0opthlem2d  10736  facwordi  10755  filtinf  10806  hashunlem  10819  zfz1isolemiso  10854  cjmulge0  10933  resqrexlemover  11054  resqrexlemdec  11055  resqrexlemlo  11057  resqrexlemcalc3  11060  resqrexlemcvg  11063  resqrexlemoverl  11065  resqrexlemglsq  11066  resqrexlemga  11067  absge0  11104  amgm2  11162  maxle1  11255  bdtrilem  11282  xrmaxifle  11289  xrmaxiflemlub  11291  xrmaxiflemval  11293  xrmax1sup  11296  xrmaxltsup  11301  xrmaxadd  11304  xrbdtri  11319  reccn2ap  11356  climle  11377  climserle  11388  isumclim2  11465  isumclim3  11466  isumge0  11473  fsumlessfi  11503  expcnvap0  11545  expcnvre  11546  explecnv  11548  absltap  11552  cvgratnnlembern  11566  cvgratnnlemnexp  11567  cvgratnnlemmn  11568  cvgratnnlemabsle  11570  cvgratnnlemfm  11572  cvgratnnlemrate  11573  mertenslemi1  11578  mertenslem2  11579  clim2divap  11583  prodmodclem3  11618  efcvg  11709  ege2le3  11714  efaddlem  11717  eftlub  11733  effsumlt  11735  ef01bndlem  11799  sin02gt0  11806  eirrap  11820  iddvdsexp  11857  dvdsadd  11878  dvdsfac  11901  dvdsmod  11903  omoe  11936  divalglemnn  11958  divalglemnqt  11960  flodddiv4t2lthalf  11977  dvdslegcd  12000  dfgcd3  12046  dvdssqim  12060  dvdsmulgcd  12061  nn0seqcvgd  12076  dvdslcm  12104  lcmgcdlem  12112  mulgcddvds  12129  qredeq  12131  cncongr2  12139  sqnprm  12171  isprm6  12182  sqpweven  12210  znege1  12213  sqrt2irrap  12215  nonsq  12242  hashdvds  12256  prmdiv  12270  odzdvds  12280  pythagtriplem4  12303  pcpre1  12327  pcdvdsb  12355  pcz  12367  pcprmpw2  12368  pcaddlem  12374  pcadd  12375  pcadd2  12376  pcmpt  12378  pcmptdvds  12380  fldivp1  12383  pcfaclem  12384  pockthlem  12391  4sqlem6  12418  4sqlem8  12420  4sqexercise1  12433  4sqexercise2  12434  4sqlemsdc  12435  4sqlem11  12436  4sqlem12  12437  4sqlem14  12439  4sqlem16  12441  ennnfonelemkh  12466  nninfdclemp1  12504  eqgen  13183  dvdsrmul1  13469  unitmulclb  13481  subrguss  13600  psmetxrge0  14309  isxmet2d  14325  mettri  14350  xmettri3  14351  mettri3  14352  xblss2ps  14381  blss2ps  14383  blss2  14384  blssps  14404  blss  14405  xmetxp  14484  ivthdec  14599  sin0pilem1  14679  sinq12gt0  14728  tangtx  14736  cosordlem  14747  cosq34lt1  14748  logdivlti  14779  logbgcd1irrap  14865  lgsdilem2  14915  2lgsoddprmlem2  14932  2sqlem3  14942  2sqlem8  14948  cvgcmp2nlemabs  15259  trilpolemclim  15263  trilpolemeq1  15267  apdifflemf  15273  apdifflemr  15274  nconstwlpolemgt0  15291