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  7082  unsnfidcel  7083  addlocprlemeq  7720  ltexprlemopl  7788  recexprlemloc  7818  cauappcvgprlemopl  7833  cauappcvgprlemladdfu  7841  cauappcvgprlem1  7846  caucvgprlemopl  7856  caucvgprlemladdfu  7864  caucvgprprlemopl  7884  caucvgprprlemexbt  7893  mulgt0sr  7965  archsr  7969  caucvgsrlemoffgt1  7986  suplocsrlemb  7993  suplocsrlem  7995  mulap0r  8762  prodgt0  8999  div4p1lem1div2  9365  mul2lt0rgt0  9956  xnn0dcle  9998  xnn0letri  9999  xleadd1a  10069  xltadd1  10072  xlt2add  10076  xposdif  10078  xlesubadd  10079  xleaddadd  10083  uzsubsubfz  10243  fzctr  10329  subfzo0  10448  exbtwnzlemstep  10467  exbtwnzlemex  10469  rebtwn2zlemstep  10472  rebtwn2z  10474  qbtwnxr  10477  xqltnle  10487  fldiv4lem1div2uz2  10526  ceilqge  10532  modqge0  10554  modqlt  10555  modqid  10571  m1modge3gt1  10593  modaddmodup  10609  addmodlteq  10620  ser3mono  10709  seqf1oglem1  10741  seqf1oglem2  10742  ser3ge0  10758  ser3le  10759  leexp1a  10816  sqgt0ap  10830  sqge0  10838  nnlesq  10865  expnbnd  10885  nn0opthlem2d  10943  facwordi  10962  filtinf  11013  hashunlem  11026  zfz1isolemiso  11061  cats1fvd  11298  cjmulge0  11400  resqrexlemover  11521  resqrexlemdec  11522  resqrexlemlo  11524  resqrexlemcalc3  11527  resqrexlemcvg  11530  resqrexlemoverl  11532  resqrexlemglsq  11533  resqrexlemga  11534  absge0  11571  amgm2  11629  maxle1  11722  bdtrilem  11750  xrmaxifle  11757  xrmaxiflemlub  11759  xrmaxiflemval  11761  xrmax1sup  11764  xrmaxltsup  11769  xrmaxadd  11772  xrbdtri  11787  reccn2ap  11824  climle  11845  climserle  11856  isumclim2  11933  isumclim3  11934  isumge0  11941  fsumlessfi  11971  expcnvap0  12013  expcnvre  12014  explecnv  12016  absltap  12020  cvgratnnlembern  12034  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratnnlemabsle  12038  cvgratnnlemfm  12040  cvgratnnlemrate  12041  mertenslemi1  12046  mertenslem2  12047  clim2divap  12051  prodmodclem3  12086  efcvg  12177  ege2le3  12182  efaddlem  12185  eftlub  12201  effsumlt  12203  ef01bndlem  12267  sin02gt0  12275  eirrap  12289  iddvdsexp  12326  dvdsadd  12347  dvdsfac  12371  dvdsmod  12373  3dvds  12375  omoe  12407  divalglemnn  12429  divalglemnqt  12431  flodddiv4t2lthalf  12450  bitsfzo  12466  bitsmod  12467  bitscmp  12469  bitsinv1lem  12472  dvdslegcd  12485  dfgcd3  12531  dvdssqim  12545  dvdsmulgcd  12546  nn0seqcvgd  12563  dvdslcm  12591  lcmgcdlem  12599  mulgcddvds  12616  qredeq  12618  cncongr2  12626  sqnprm  12658  isprm6  12669  sqpweven  12697  znege1  12700  sqrt2irrap  12702  nonsq  12729  hashdvds  12743  prmdiv  12757  odzdvds  12768  pythagtriplem4  12791  pcpre1  12815  pcdvdsb  12843  pcz  12855  pcprmpw2  12856  pcaddlem  12862  pcadd  12863  pcadd2  12864  pcmpt  12866  pcmptdvds  12868  fldivp1  12871  pcfaclem  12872  pockthlem  12879  4sqlem6  12906  4sqlem8  12908  4sqexercise1  12921  4sqexercise2  12922  4sqlemsdc  12923  4sqlem11  12924  4sqlem12  12925  4sqlem14  12927  4sqlem16  12929  ennnfonelemkh  12983  nninfdclemp1  13021  eqgen  13764  dvdsrmul1  14066  unitmulclb  14078  subrguss  14200  znidom  14621  znunit  14623  mplsubgfilemcl  14663  psmetxrge0  15006  isxmet2d  15022  mettri  15047  xmettri3  15048  mettri3  15049  xblss2ps  15078  blss2ps  15080  blss2  15081  blssps  15101  blss  15102  xmetxp  15181  ivthdec  15318  ivthreinc  15319  hoverb  15322  hovergt0  15324  sin0pilem1  15455  sinq12gt0  15504  tangtx  15512  cosordlem  15523  cosq34lt1  15524  logdivlti  15555  logbgcd1irrap  15644  perfectlem1  15673  lgsdilem2  15715  gausslemma2dlem1f1o  15739  lgsquadlem1  15756  2lgsoddprmlem2  15785  2sqlem3  15796  2sqlem8  15802  usgrsizedgen  16011  cvgcmp2nlemabs  16400  trilpolemclim  16404  trilpolemeq1  16408  apdifflemf  16414  apdifflemr  16415  nconstwlpolemgt0  16432