Theorem breqtrrd 4114

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

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4086

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  frirrg  4445  fidcen  7081  unsnfidcex  7105  unsnfidcel  7106  addlocprlemeq  7743  ltexprlemopl  7811  recexprlemloc  7841  cauappcvgprlemopl  7856  cauappcvgprlemladdfu  7864  cauappcvgprlem1  7869  caucvgprlemopl  7879  caucvgprlemladdfu  7887  caucvgprprlemopl  7907  caucvgprprlemexbt  7916  mulgt0sr  7988  archsr  7992  caucvgsrlemoffgt1  8009  suplocsrlemb  8016  suplocsrlem  8018  mulap0r  8785  prodgt0  9022  div4p1lem1div2  9388  mul2lt0rgt0  9985  xnn0dcle  10027  xnn0letri  10028  xleadd1a  10098  xltadd1  10101  xlt2add  10105  xposdif  10107  xlesubadd  10108  xleaddadd  10112  uzsubsubfz  10272  fzctr  10358  subfzo0  10478  exbtwnzlemstep  10497  exbtwnzlemex  10499  rebtwn2zlemstep  10502  rebtwn2z  10504  qbtwnxr  10507  xqltnle  10517  fldiv4lem1div2uz2  10556  ceilqge  10562  modqge0  10584  modqlt  10585  modqid  10601  m1modge3gt1  10623  modaddmodup  10639  addmodlteq  10650  ser3mono  10739  seqf1oglem1  10771  seqf1oglem2  10772  ser3ge0  10788  ser3le  10789  leexp1a  10846  sqgt0ap  10860  sqge0  10868  nnlesq  10895  expnbnd  10915  nn0opthlem2d  10973  facwordi  10992  filtinf  11043  hashunlem  11057  zfz1isolemiso  11093  cats1fvd  11337  cjmulge0  11440  resqrexlemover  11561  resqrexlemdec  11562  resqrexlemlo  11564  resqrexlemcalc3  11567  resqrexlemcvg  11570  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemga  11574  absge0  11611  amgm2  11669  maxle1  11762  bdtrilem  11790  xrmaxifle  11797  xrmaxiflemlub  11799  xrmaxiflemval  11801  xrmax1sup  11804  xrmaxltsup  11809  xrmaxadd  11812  xrbdtri  11827  reccn2ap  11864  climle  11885  climserle  11896  isumclim2  11973  isumclim3  11974  isumge0  11981  fsumlessfi  12011  expcnvap0  12053  expcnvre  12054  explecnv  12056  absltap  12060  cvgratnnlembern  12074  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemabsle  12078  cvgratnnlemfm  12080  cvgratnnlemrate  12081  mertenslemi1  12086  mertenslem2  12087  clim2divap  12091  prodmodclem3  12126  efcvg  12217  ege2le3  12222  efaddlem  12225  eftlub  12241  effsumlt  12243  ef01bndlem  12307  sin02gt0  12315  eirrap  12329  iddvdsexp  12366  dvdsadd  12387  dvdsfac  12411  dvdsmod  12413  3dvds  12415  omoe  12447  divalglemnn  12469  divalglemnqt  12471  flodddiv4t2lthalf  12490  bitsfzo  12506  bitsmod  12507  bitscmp  12509  bitsinv1lem  12512  dvdslegcd  12525  dfgcd3  12571  dvdssqim  12585  dvdsmulgcd  12586  nn0seqcvgd  12603  dvdslcm  12631  lcmgcdlem  12639  mulgcddvds  12656  qredeq  12658  cncongr2  12666  sqnprm  12698  isprm6  12709  sqpweven  12737  znege1  12740  sqrt2irrap  12742  nonsq  12769  hashdvds  12783  prmdiv  12797  odzdvds  12808  pythagtriplem4  12831  pcpre1  12855  pcdvdsb  12883  pcz  12895  pcprmpw2  12896  pcaddlem  12902  pcadd  12903  pcadd2  12904  pcmpt  12906  pcmptdvds  12908  fldivp1  12911  pcfaclem  12912  pockthlem  12919  4sqlem6  12946  4sqlem8  12948  4sqexercise1  12961  4sqexercise2  12962  4sqlemsdc  12963  4sqlem11  12964  4sqlem12  12965  4sqlem14  12967  4sqlem16  12969  ennnfonelemkh  13023  nninfdclemp1  13061  eqgen  13804  dvdsrmul1  14106  unitmulclb  14118  subrguss  14240  znidom  14661  znunit  14663  mplsubgfilemcl  14703  psmetxrge0  15046  isxmet2d  15062  mettri  15087  xmettri3  15088  mettri3  15089  xblss2ps  15118  blss2ps  15120  blss2  15121  blssps  15141  blss  15142  xmetxp  15221  ivthdec  15358  ivthreinc  15359  hoverb  15362  hovergt0  15364  sin0pilem1  15495  sinq12gt0  15544  tangtx  15552  cosordlem  15563  cosq34lt1  15564  logdivlti  15595  logbgcd1irrap  15684  perfectlem1  15713  lgsdilem2  15755  gausslemma2dlem1f1o  15779  lgsquadlem1  15796  2lgsoddprmlem2  15825  2sqlem3  15836  2sqlem8  15842  usgrsizedgen  16052  cvgcmp2nlemabs  16572  trilpolemclim  16576  trilpolemeq1  16580  apdifflemf  16586  apdifflemr  16587  nconstwlpolemgt0  16604