Theorem breqtrrd 3921

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

Syntax hints:   → wi 4   = wceq 1314   class class class wbr 3895

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-un 3041  df-sn 3499  df-pr 3500  df-op 3502  df-br 3896

This theorem is referenced by:  frirrg  4232  unsnfidcex  6761  unsnfidcel  6762  addlocprlemeq  7289  ltexprlemopl  7357  recexprlemloc  7387  cauappcvgprlemopl  7402  cauappcvgprlemladdfu  7410  cauappcvgprlem1  7415  caucvgprlemopl  7425  caucvgprlemladdfu  7433  caucvgprprlemopl  7453  caucvgprprlemexbt  7462  mulgt0sr  7520  archsr  7524  caucvgsrlemoffgt1  7541  mulap0r  8295  prodgt0  8520  div4p1lem1div2  8877  xleadd1a  9549  xltadd1  9552  xlt2add  9556  xposdif  9558  xlesubadd  9559  xleaddadd  9563  uzsubsubfz  9720  fzctr  9803  subfzo0  9912  exbtwnzlemstep  9918  exbtwnzlemex  9920  rebtwn2zlemstep  9923  rebtwn2z  9925  qbtwnxr  9928  ceilqge  9976  modqge0  9998  modqlt  9999  modqid  10015  m1modge3gt1  10037  modaddmodup  10053  addmodlteq  10064  ser3mono  10144  ser3ge0  10183  ser3le  10184  leexp1a  10241  sqgt0ap  10254  sqge0  10262  nnlesq  10289  expnbnd  10308  nn0opthlem2d  10360  facwordi  10379  filtinf  10431  hashunlem  10443  zfz1isolemiso  10475  cjmulge0  10554  resqrexlemover  10674  resqrexlemdec  10675  resqrexlemlo  10677  resqrexlemcalc3  10680  resqrexlemcvg  10683  resqrexlemoverl  10685  resqrexlemglsq  10686  resqrexlemga  10687  absge0  10724  amgm2  10782  maxle1  10875  bdtrilem  10902  xrmaxifle  10907  xrmaxiflemlub  10909  xrmaxiflemval  10911  xrmax1sup  10914  xrmaxltsup  10919  xrmaxadd  10922  xrbdtri  10937  reccn2ap  10974  climle  10995  climserle  11006  isumclim2  11083  isumclim3  11084  isumge0  11091  fsumlessfi  11121  expcnvap0  11163  expcnvre  11164  explecnv  11166  absltap  11170  cvgratnnlembern  11184  cvgratnnlemnexp  11185  cvgratnnlemmn  11186  cvgratnnlemabsle  11188  cvgratnnlemfm  11190  cvgratnnlemrate  11191  mertenslemi1  11196  mertenslem2  11197  efcvg  11223  ege2le3  11228  efaddlem  11231  eftlub  11247  effsumlt  11249  ef01bndlem  11314  sin02gt0  11321  eirrap  11332  iddvdsexp  11365  dvdsadd  11384  dvdsfac  11406  dvdsmod  11408  omoe  11441  divalglemnn  11463  divalglemnqt  11465  flodddiv4t2lthalf  11482  dvdslegcd  11501  dfgcd3  11544  dvdssqim  11558  dvdsmulgcd  11559  nn0seqcvgd  11568  dvdslcm  11596  lcmgcdlem  11604  mulgcddvds  11621  qredeq  11623  cncongr2  11631  sqnprm  11662  isprm6  11671  sqpweven  11698  znege1  11701  sqrt2irrap  11703  nonsq  11730  hashdvds  11742  ennnfonelemkh  11770  psmetxrge0  12321  isxmet2d  12337  mettri  12362  xmettri3  12363  mettri3  12364  xblss2ps  12393  blss2ps  12395  blss2  12396  blssps  12416  blss  12417  xmetxp  12496  cvgcmp2nlemabs  12919  trilpolemclim  12921  trilpolemeq1  12925