Theorem breqtrrd 4116

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

Syntax hints:   → wi 4   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  frirrg  4447  fidcen  7088  unsnfidcex  7112  unsnfidcel  7113  addlocprlemeq  7753  ltexprlemopl  7821  recexprlemloc  7851  cauappcvgprlemopl  7866  cauappcvgprlemladdfu  7874  cauappcvgprlem1  7879  caucvgprlemopl  7889  caucvgprlemladdfu  7897  caucvgprprlemopl  7917  caucvgprprlemexbt  7926  mulgt0sr  7998  archsr  8002  caucvgsrlemoffgt1  8019  suplocsrlemb  8026  suplocsrlem  8028  mulap0r  8795  prodgt0  9032  div4p1lem1div2  9398  mul2lt0rgt0  9995  xnn0dcle  10037  xnn0letri  10038  xleadd1a  10108  xltadd1  10111  xlt2add  10115  xposdif  10117  xlesubadd  10118  xleaddadd  10122  uzsubsubfz  10282  fzctr  10368  subfzo0  10489  exbtwnzlemstep  10508  exbtwnzlemex  10510  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnxr  10518  xqltnle  10528  fldiv4lem1div2uz2  10567  ceilqge  10573  modqge0  10595  modqlt  10596  modqid  10612  m1modge3gt1  10634  modaddmodup  10650  addmodlteq  10661  ser3mono  10750  seqf1oglem1  10782  seqf1oglem2  10783  ser3ge0  10799  ser3le  10800  leexp1a  10857  sqgt0ap  10871  sqge0  10879  nnlesq  10906  expnbnd  10926  nn0opthlem2d  10984  facwordi  11003  filtinf  11054  hashunlem  11068  zfz1isolemiso  11104  cats1fvd  11351  cjmulge0  11467  resqrexlemover  11588  resqrexlemdec  11589  resqrexlemlo  11591  resqrexlemcalc3  11594  resqrexlemcvg  11597  resqrexlemoverl  11599  resqrexlemglsq  11600  resqrexlemga  11601  absge0  11638  amgm2  11696  maxle1  11789  bdtrilem  11817  xrmaxifle  11824  xrmaxiflemlub  11826  xrmaxiflemval  11828  xrmax1sup  11831  xrmaxltsup  11836  xrmaxadd  11839  xrbdtri  11854  reccn2ap  11891  climle  11912  climserle  11923  isumclim2  12001  isumclim3  12002  isumge0  12009  fsumlessfi  12039  expcnvap0  12081  expcnvre  12082  explecnv  12084  absltap  12088  cvgratnnlembern  12102  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  cvgratnnlemabsle  12106  cvgratnnlemfm  12108  cvgratnnlemrate  12109  mertenslemi1  12114  mertenslem2  12115  clim2divap  12119  prodmodclem3  12154  efcvg  12245  ege2le3  12250  efaddlem  12253  eftlub  12269  effsumlt  12271  ef01bndlem  12335  sin02gt0  12343  eirrap  12357  iddvdsexp  12394  dvdsadd  12415  dvdsfac  12439  dvdsmod  12441  3dvds  12443  omoe  12475  divalglemnn  12497  divalglemnqt  12499  flodddiv4t2lthalf  12518  bitsfzo  12534  bitsmod  12535  bitscmp  12537  bitsinv1lem  12540  dvdslegcd  12553  dfgcd3  12599  dvdssqim  12613  dvdsmulgcd  12614  nn0seqcvgd  12631  dvdslcm  12659  lcmgcdlem  12667  mulgcddvds  12684  qredeq  12686  cncongr2  12694  sqnprm  12726  isprm6  12737  sqpweven  12765  znege1  12768  sqrt2irrap  12770  nonsq  12797  hashdvds  12811  prmdiv  12825  odzdvds  12836  pythagtriplem4  12859  pcpre1  12883  pcdvdsb  12911  pcz  12923  pcprmpw2  12924  pcaddlem  12930  pcadd  12931  pcadd2  12932  pcmpt  12934  pcmptdvds  12936  fldivp1  12939  pcfaclem  12940  pockthlem  12947  4sqlem6  12974  4sqlem8  12976  4sqexercise1  12989  4sqexercise2  12990  4sqlemsdc  12991  4sqlem11  12992  4sqlem12  12993  4sqlem14  12995  4sqlem16  12997  ennnfonelemkh  13051  nninfdclemp1  13089  eqgen  13832  dvdsrmul1  14135  unitmulclb  14147  subrguss  14269  znidom  14690  znunit  14692  mplsubgfilemcl  14732  psmetxrge0  15075  isxmet2d  15091  mettri  15116  xmettri3  15117  mettri3  15118  xblss2ps  15147  blss2ps  15149  blss2  15150  blssps  15170  blss  15171  xmetxp  15250  ivthdec  15387  ivthreinc  15388  hoverb  15391  hovergt0  15393  sin0pilem1  15524  sinq12gt0  15573  tangtx  15581  cosordlem  15592  cosq34lt1  15593  logdivlti  15624  logbgcd1irrap  15713  perfectlem1  15742  lgsdilem2  15784  gausslemma2dlem1f1o  15808  lgsquadlem1  15825  2lgsoddprmlem2  15854  2sqlem3  15865  2sqlem8  15871  usgrsizedgen  16083  cvgcmp2nlemabs  16687  trilpolemclim  16691  trilpolemeq1  16695  apdifflemf  16701  apdifflemr  16702  nconstwlpolemgt0  16720