Theorem breqtrrd 4121

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

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  frirrg  4453  fidcen  7131  unsnfidcex  7155  unsnfidcel  7156  addlocprlemeq  7813  ltexprlemopl  7881  recexprlemloc  7911  cauappcvgprlemopl  7926  cauappcvgprlemladdfu  7934  cauappcvgprlem1  7939  caucvgprlemopl  7949  caucvgprlemladdfu  7957  caucvgprprlemopl  7977  caucvgprprlemexbt  7986  mulgt0sr  8058  archsr  8062  caucvgsrlemoffgt1  8079  suplocsrlemb  8086  suplocsrlem  8088  mulap0r  8854  prodgt0  9091  div4p1lem1div2  9457  mul2lt0rgt0  10056  xnn0dcle  10098  xnn0letri  10099  xleadd1a  10169  xltadd1  10172  xlt2add  10176  xposdif  10178  xlesubadd  10179  xleaddadd  10183  uzsubsubfz  10344  fzctr  10430  subfzo0  10551  exbtwnzlemstep  10570  exbtwnzlemex  10572  rebtwn2zlemstep  10575  rebtwn2z  10577  qbtwnxr  10580  xqltnle  10590  fldiv4lem1div2uz2  10629  ceilqge  10635  modqge0  10657  modqlt  10658  modqid  10674  m1modge3gt1  10696  modaddmodup  10712  addmodlteq  10723  ser3mono  10812  seqf1oglem1  10844  seqf1oglem2  10845  ser3ge0  10861  ser3le  10862  leexp1a  10919  sqgt0ap  10933  sqge0  10941  nnlesq  10968  expnbnd  10988  nn0opthlem2d  11046  facwordi  11065  filtinf  11116  hashunlem  11130  zfz1isolemiso  11166  cats1fvd  11413  cjmulge0  11529  resqrexlemover  11650  resqrexlemdec  11651  resqrexlemlo  11653  resqrexlemcalc3  11656  resqrexlemcvg  11659  resqrexlemoverl  11661  resqrexlemglsq  11662  resqrexlemga  11663  absge0  11700  amgm2  11758  maxle1  11851  bdtrilem  11879  xrmaxifle  11886  xrmaxiflemlub  11888  xrmaxiflemval  11890  xrmax1sup  11893  xrmaxltsup  11898  xrmaxadd  11901  xrbdtri  11916  reccn2ap  11953  climle  11974  climserle  11985  isumclim2  12063  isumclim3  12064  isumge0  12071  fsumlessfi  12101  expcnvap0  12143  expcnvre  12144  explecnv  12146  absltap  12150  cvgratnnlembern  12164  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  cvgratnnlemabsle  12168  cvgratnnlemfm  12170  cvgratnnlemrate  12171  mertenslemi1  12176  mertenslem2  12177  clim2divap  12181  prodmodclem3  12216  efcvg  12307  ege2le3  12312  efaddlem  12315  eftlub  12331  effsumlt  12333  ef01bndlem  12397  sin02gt0  12405  eirrap  12419  iddvdsexp  12456  dvdsadd  12477  dvdsfac  12501  dvdsmod  12503  3dvds  12505  omoe  12537  divalglemnn  12559  divalglemnqt  12561  flodddiv4t2lthalf  12580  bitsfzo  12596  bitsmod  12597  bitscmp  12599  bitsinv1lem  12602  dvdslegcd  12615  dfgcd3  12661  dvdssqim  12675  dvdsmulgcd  12676  nn0seqcvgd  12693  dvdslcm  12721  lcmgcdlem  12729  mulgcddvds  12746  qredeq  12748  cncongr2  12756  sqnprm  12788  isprm6  12799  sqpweven  12827  znege1  12830  sqrt2irrap  12832  nonsq  12859  hashdvds  12873  prmdiv  12887  odzdvds  12898  pythagtriplem4  12921  pcpre1  12945  pcdvdsb  12973  pcz  12985  pcprmpw2  12986  pcaddlem  12992  pcadd  12993  pcadd2  12994  pcmpt  12996  pcmptdvds  12998  fldivp1  13001  pcfaclem  13002  pockthlem  13009  4sqlem6  13036  4sqlem8  13038  4sqexercise1  13051  4sqexercise2  13052  4sqlemsdc  13053  4sqlem11  13054  4sqlem12  13055  4sqlem14  13057  4sqlem16  13059  ennnfonelemkh  13113  nninfdclemp1  13151  eqgen  13894  dvdsrmul1  14197  unitmulclb  14209  subrguss  14331  znidom  14753  znunit  14755  mplsubgfilemcl  14800  psmetxrge0  15143  isxmet2d  15159  mettri  15184  xmettri3  15185  mettri3  15186  xblss2ps  15215  blss2ps  15217  blss2  15218  blssps  15238  blss  15239  xmetxp  15318  ivthdec  15455  ivthreinc  15456  hoverb  15459  hovergt0  15461  sin0pilem1  15592  sinq12gt0  15641  tangtx  15649  cosordlem  15660  cosq34lt1  15661  logdivlti  15692  logbgcd1irrap  15781  perfectlem1  15813  lgsdilem2  15855  gausslemma2dlem1f1o  15879  lgsquadlem1  15896  2lgsoddprmlem2  15925  2sqlem3  15936  2sqlem8  15942  usgrsizedgen  16154  cvgcmp2nlemabs  16764  trilpolemclim  16768  trilpolemeq1  16772  apdifflemf  16778  apdifflemr  16779  nconstwlpolemgt0  16797