Theorem breqtrrd 4087

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  frirrg  4415  unsnfidcex  7043  unsnfidcel  7044  addlocprlemeq  7681  ltexprlemopl  7749  recexprlemloc  7779  cauappcvgprlemopl  7794  cauappcvgprlemladdfu  7802  cauappcvgprlem1  7807  caucvgprlemopl  7817  caucvgprlemladdfu  7825  caucvgprprlemopl  7845  caucvgprprlemexbt  7854  mulgt0sr  7926  archsr  7930  caucvgsrlemoffgt1  7947  suplocsrlemb  7954  suplocsrlem  7956  mulap0r  8723  prodgt0  8960  div4p1lem1div2  9326  mul2lt0rgt0  9917  xnn0dcle  9959  xnn0letri  9960  xleadd1a  10030  xltadd1  10033  xlt2add  10037  xposdif  10039  xlesubadd  10040  xleaddadd  10044  uzsubsubfz  10204  fzctr  10290  subfzo0  10408  exbtwnzlemstep  10427  exbtwnzlemex  10429  rebtwn2zlemstep  10432  rebtwn2z  10434  qbtwnxr  10437  xqltnle  10447  fldiv4lem1div2uz2  10486  ceilqge  10492  modqge0  10514  modqlt  10515  modqid  10531  m1modge3gt1  10553  modaddmodup  10569  addmodlteq  10580  ser3mono  10669  seqf1oglem1  10701  seqf1oglem2  10702  ser3ge0  10718  ser3le  10719  leexp1a  10776  sqgt0ap  10790  sqge0  10798  nnlesq  10825  expnbnd  10845  nn0opthlem2d  10903  facwordi  10922  filtinf  10973  hashunlem  10986  zfz1isolemiso  11021  cjmulge0  11315  resqrexlemover  11436  resqrexlemdec  11437  resqrexlemlo  11439  resqrexlemcalc3  11442  resqrexlemcvg  11445  resqrexlemoverl  11447  resqrexlemglsq  11448  resqrexlemga  11449  absge0  11486  amgm2  11544  maxle1  11637  bdtrilem  11665  xrmaxifle  11672  xrmaxiflemlub  11674  xrmaxiflemval  11676  xrmax1sup  11679  xrmaxltsup  11684  xrmaxadd  11687  xrbdtri  11702  reccn2ap  11739  climle  11760  climserle  11771  isumclim2  11848  isumclim3  11849  isumge0  11856  fsumlessfi  11886  expcnvap0  11928  expcnvre  11929  explecnv  11931  absltap  11935  cvgratnnlembern  11949  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  cvgratnnlemabsle  11953  cvgratnnlemfm  11955  cvgratnnlemrate  11956  mertenslemi1  11961  mertenslem2  11962  clim2divap  11966  prodmodclem3  12001  efcvg  12092  ege2le3  12097  efaddlem  12100  eftlub  12116  effsumlt  12118  ef01bndlem  12182  sin02gt0  12190  eirrap  12204  iddvdsexp  12241  dvdsadd  12262  dvdsfac  12286  dvdsmod  12288  3dvds  12290  omoe  12322  divalglemnn  12344  divalglemnqt  12346  flodddiv4t2lthalf  12365  bitsfzo  12381  bitsmod  12382  bitscmp  12384  bitsinv1lem  12387  dvdslegcd  12400  dfgcd3  12446  dvdssqim  12460  dvdsmulgcd  12461  nn0seqcvgd  12478  dvdslcm  12506  lcmgcdlem  12514  mulgcddvds  12531  qredeq  12533  cncongr2  12541  sqnprm  12573  isprm6  12584  sqpweven  12612  znege1  12615  sqrt2irrap  12617  nonsq  12644  hashdvds  12658  prmdiv  12672  odzdvds  12683  pythagtriplem4  12706  pcpre1  12730  pcdvdsb  12758  pcz  12770  pcprmpw2  12771  pcaddlem  12777  pcadd  12778  pcadd2  12779  pcmpt  12781  pcmptdvds  12783  fldivp1  12786  pcfaclem  12787  pockthlem  12794  4sqlem6  12821  4sqlem8  12823  4sqexercise1  12836  4sqexercise2  12837  4sqlemsdc  12838  4sqlem11  12839  4sqlem12  12840  4sqlem14  12842  4sqlem16  12844  ennnfonelemkh  12898  nninfdclemp1  12936  eqgen  13678  dvdsrmul1  13979  unitmulclb  13991  subrguss  14113  znidom  14534  znunit  14536  mplsubgfilemcl  14576  psmetxrge0  14919  isxmet2d  14935  mettri  14960  xmettri3  14961  mettri3  14962  xblss2ps  14991  blss2ps  14993  blss2  14994  blssps  15014  blss  15015  xmetxp  15094  ivthdec  15231  ivthreinc  15232  hoverb  15235  hovergt0  15237  sin0pilem1  15368  sinq12gt0  15417  tangtx  15425  cosordlem  15436  cosq34lt1  15437  logdivlti  15468  logbgcd1irrap  15557  perfectlem1  15586  lgsdilem2  15628  gausslemma2dlem1f1o  15652  lgsquadlem1  15669  2lgsoddprmlem2  15698  2sqlem3  15709  2sqlem8  15715  cvgcmp2nlemabs  16173  trilpolemclim  16177  trilpolemeq1  16181  apdifflemf  16187  apdifflemr  16188  nconstwlpolemgt0  16205