Theorem breqtrrd 4111

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 4109	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  frirrg  4441  fidcen  7069  unsnfidcex  7093  unsnfidcel  7094  addlocprlemeq  7731  ltexprlemopl  7799  recexprlemloc  7829  cauappcvgprlemopl  7844  cauappcvgprlemladdfu  7852  cauappcvgprlem1  7857  caucvgprlemopl  7867  caucvgprlemladdfu  7875  caucvgprprlemopl  7895  caucvgprprlemexbt  7904  mulgt0sr  7976  archsr  7980  caucvgsrlemoffgt1  7997  suplocsrlemb  8004  suplocsrlem  8006  mulap0r  8773  prodgt0  9010  div4p1lem1div2  9376  mul2lt0rgt0  9968  xnn0dcle  10010  xnn0letri  10011  xleadd1a  10081  xltadd1  10084  xlt2add  10088  xposdif  10090  xlesubadd  10091  xleaddadd  10095  uzsubsubfz  10255  fzctr  10341  subfzo0  10460  exbtwnzlemstep  10479  exbtwnzlemex  10481  rebtwn2zlemstep  10484  rebtwn2z  10486  qbtwnxr  10489  xqltnle  10499  fldiv4lem1div2uz2  10538  ceilqge  10544  modqge0  10566  modqlt  10567  modqid  10583  m1modge3gt1  10605  modaddmodup  10621  addmodlteq  10632  ser3mono  10721  seqf1oglem1  10753  seqf1oglem2  10754  ser3ge0  10770  ser3le  10771  leexp1a  10828  sqgt0ap  10842  sqge0  10850  nnlesq  10877  expnbnd  10897  nn0opthlem2d  10955  facwordi  10974  filtinf  11025  hashunlem  11038  zfz1isolemiso  11074  cats1fvd  11314  cjmulge0  11416  resqrexlemover  11537  resqrexlemdec  11538  resqrexlemlo  11540  resqrexlemcalc3  11543  resqrexlemcvg  11546  resqrexlemoverl  11548  resqrexlemglsq  11549  resqrexlemga  11550  absge0  11587  amgm2  11645  maxle1  11738  bdtrilem  11766  xrmaxifle  11773  xrmaxiflemlub  11775  xrmaxiflemval  11777  xrmax1sup  11780  xrmaxltsup  11785  xrmaxadd  11788  xrbdtri  11803  reccn2ap  11840  climle  11861  climserle  11872  isumclim2  11949  isumclim3  11950  isumge0  11957  fsumlessfi  11987  expcnvap0  12029  expcnvre  12030  explecnv  12032  absltap  12036  cvgratnnlembern  12050  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  cvgratnnlemabsle  12054  cvgratnnlemfm  12056  cvgratnnlemrate  12057  mertenslemi1  12062  mertenslem2  12063  clim2divap  12067  prodmodclem3  12102  efcvg  12193  ege2le3  12198  efaddlem  12201  eftlub  12217  effsumlt  12219  ef01bndlem  12283  sin02gt0  12291  eirrap  12305  iddvdsexp  12342  dvdsadd  12363  dvdsfac  12387  dvdsmod  12389  3dvds  12391  omoe  12423  divalglemnn  12445  divalglemnqt  12447  flodddiv4t2lthalf  12466  bitsfzo  12482  bitsmod  12483  bitscmp  12485  bitsinv1lem  12488  dvdslegcd  12501  dfgcd3  12547  dvdssqim  12561  dvdsmulgcd  12562  nn0seqcvgd  12579  dvdslcm  12607  lcmgcdlem  12615  mulgcddvds  12632  qredeq  12634  cncongr2  12642  sqnprm  12674  isprm6  12685  sqpweven  12713  znege1  12716  sqrt2irrap  12718  nonsq  12745  hashdvds  12759  prmdiv  12773  odzdvds  12784  pythagtriplem4  12807  pcpre1  12831  pcdvdsb  12859  pcz  12871  pcprmpw2  12872  pcaddlem  12878  pcadd  12879  pcadd2  12880  pcmpt  12882  pcmptdvds  12884  fldivp1  12887  pcfaclem  12888  pockthlem  12895  4sqlem6  12922  4sqlem8  12924  4sqexercise1  12937  4sqexercise2  12938  4sqlemsdc  12939  4sqlem11  12940  4sqlem12  12941  4sqlem14  12943  4sqlem16  12945  ennnfonelemkh  12999  nninfdclemp1  13037  eqgen  13780  dvdsrmul1  14082  unitmulclb  14094  subrguss  14216  znidom  14637  znunit  14639  mplsubgfilemcl  14679  psmetxrge0  15022  isxmet2d  15038  mettri  15063  xmettri3  15064  mettri3  15065  xblss2ps  15094  blss2ps  15096  blss2  15097  blssps  15117  blss  15118  xmetxp  15197  ivthdec  15334  ivthreinc  15335  hoverb  15338  hovergt0  15340  sin0pilem1  15471  sinq12gt0  15520  tangtx  15528  cosordlem  15539  cosq34lt1  15540  logdivlti  15571  logbgcd1irrap  15660  perfectlem1  15689  lgsdilem2  15731  gausslemma2dlem1f1o  15755  lgsquadlem1  15772  2lgsoddprmlem2  15801  2sqlem3  15812  2sqlem8  15818  usgrsizedgen  16027  cvgcmp2nlemabs  16488  trilpolemclim  16492  trilpolemeq1  16496  apdifflemf  16502  apdifflemr  16503  nconstwlpolemgt0  16520