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  unsnfidcex  7090  unsnfidcel  7091  addlocprlemeq  7728  ltexprlemopl  7796  recexprlemloc  7826  cauappcvgprlemopl  7841  cauappcvgprlemladdfu  7849  cauappcvgprlem1  7854  caucvgprlemopl  7864  caucvgprlemladdfu  7872  caucvgprprlemopl  7892  caucvgprprlemexbt  7901  mulgt0sr  7973  archsr  7977  caucvgsrlemoffgt1  7994  suplocsrlemb  8001  suplocsrlem  8003  mulap0r  8770  prodgt0  9007  div4p1lem1div2  9373  mul2lt0rgt0  9964  xnn0dcle  10006  xnn0letri  10007  xleadd1a  10077  xltadd1  10080  xlt2add  10084  xposdif  10086  xlesubadd  10087  xleaddadd  10091  uzsubsubfz  10251  fzctr  10337  subfzo0  10456  exbtwnzlemstep  10475  exbtwnzlemex  10477  rebtwn2zlemstep  10480  rebtwn2z  10482  qbtwnxr  10485  xqltnle  10495  fldiv4lem1div2uz2  10534  ceilqge  10540  modqge0  10562  modqlt  10563  modqid  10579  m1modge3gt1  10601  modaddmodup  10617  addmodlteq  10628  ser3mono  10717  seqf1oglem1  10749  seqf1oglem2  10750  ser3ge0  10766  ser3le  10767  leexp1a  10824  sqgt0ap  10838  sqge0  10846  nnlesq  10873  expnbnd  10893  nn0opthlem2d  10951  facwordi  10970  filtinf  11021  hashunlem  11034  zfz1isolemiso  11069  cats1fvd  11306  cjmulge0  11408  resqrexlemover  11529  resqrexlemdec  11530  resqrexlemlo  11532  resqrexlemcalc3  11535  resqrexlemcvg  11538  resqrexlemoverl  11540  resqrexlemglsq  11541  resqrexlemga  11542  absge0  11579  amgm2  11637  maxle1  11730  bdtrilem  11758  xrmaxifle  11765  xrmaxiflemlub  11767  xrmaxiflemval  11769  xrmax1sup  11772  xrmaxltsup  11777  xrmaxadd  11780  xrbdtri  11795  reccn2ap  11832  climle  11853  climserle  11864  isumclim2  11941  isumclim3  11942  isumge0  11949  fsumlessfi  11979  expcnvap0  12021  expcnvre  12022  explecnv  12024  absltap  12028  cvgratnnlembern  12042  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  cvgratnnlemabsle  12046  cvgratnnlemfm  12048  cvgratnnlemrate  12049  mertenslemi1  12054  mertenslem2  12055  clim2divap  12059  prodmodclem3  12094  efcvg  12185  ege2le3  12190  efaddlem  12193  eftlub  12209  effsumlt  12211  ef01bndlem  12275  sin02gt0  12283  eirrap  12297  iddvdsexp  12334  dvdsadd  12355  dvdsfac  12379  dvdsmod  12381  3dvds  12383  omoe  12415  divalglemnn  12437  divalglemnqt  12439  flodddiv4t2lthalf  12458  bitsfzo  12474  bitsmod  12475  bitscmp  12477  bitsinv1lem  12480  dvdslegcd  12493  dfgcd3  12539  dvdssqim  12553  dvdsmulgcd  12554  nn0seqcvgd  12571  dvdslcm  12599  lcmgcdlem  12607  mulgcddvds  12624  qredeq  12626  cncongr2  12634  sqnprm  12666  isprm6  12677  sqpweven  12705  znege1  12708  sqrt2irrap  12710  nonsq  12737  hashdvds  12751  prmdiv  12765  odzdvds  12776  pythagtriplem4  12799  pcpre1  12823  pcdvdsb  12851  pcz  12863  pcprmpw2  12864  pcaddlem  12870  pcadd  12871  pcadd2  12872  pcmpt  12874  pcmptdvds  12876  fldivp1  12879  pcfaclem  12880  pockthlem  12887  4sqlem6  12914  4sqlem8  12916  4sqexercise1  12929  4sqexercise2  12930  4sqlemsdc  12931  4sqlem11  12932  4sqlem12  12933  4sqlem14  12935  4sqlem16  12937  ennnfonelemkh  12991  nninfdclemp1  13029  eqgen  13772  dvdsrmul1  14074  unitmulclb  14086  subrguss  14208  znidom  14629  znunit  14631  mplsubgfilemcl  14671  psmetxrge0  15014  isxmet2d  15030  mettri  15055  xmettri3  15056  mettri3  15057  xblss2ps  15086  blss2ps  15088  blss2  15089  blssps  15109  blss  15110  xmetxp  15189  ivthdec  15326  ivthreinc  15327  hoverb  15330  hovergt0  15332  sin0pilem1  15463  sinq12gt0  15512  tangtx  15520  cosordlem  15531  cosq34lt1  15532  logdivlti  15563  logbgcd1irrap  15652  perfectlem1  15681  lgsdilem2  15723  gausslemma2dlem1f1o  15747  lgsquadlem1  15764  2lgsoddprmlem2  15793  2sqlem3  15804  2sqlem8  15810  usgrsizedgen  16019  fidcen  16379  cvgcmp2nlemabs  16430  trilpolemclim  16434  trilpolemeq1  16438  apdifflemf  16444  apdifflemr  16445  nconstwlpolemgt0  16462