Theorem breqtrrd 4026

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

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 3998

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999

This theorem is referenced by:  frirrg  4344  unsnfidcex  6909  unsnfidcel  6910  addlocprlemeq  7507  ltexprlemopl  7575  recexprlemloc  7605  cauappcvgprlemopl  7620  cauappcvgprlemladdfu  7628  cauappcvgprlem1  7633  caucvgprlemopl  7643  caucvgprlemladdfu  7651  caucvgprprlemopl  7671  caucvgprprlemexbt  7680  mulgt0sr  7752  archsr  7756  caucvgsrlemoffgt1  7773  suplocsrlemb  7780  suplocsrlem  7782  mulap0r  8546  prodgt0  8780  div4p1lem1div2  9143  mul2lt0rgt0  9729  xnn0dcle  9771  xnn0letri  9772  xleadd1a  9842  xltadd1  9845  xlt2add  9849  xposdif  9851  xlesubadd  9852  xleaddadd  9856  uzsubsubfz  10015  fzctr  10101  subfzo0  10210  exbtwnzlemstep  10216  exbtwnzlemex  10218  rebtwn2zlemstep  10221  rebtwn2z  10223  qbtwnxr  10226  ceilqge  10278  modqge0  10300  modqlt  10301  modqid  10317  m1modge3gt1  10339  modaddmodup  10355  addmodlteq  10366  ser3mono  10446  ser3ge0  10485  ser3le  10486  leexp1a  10543  sqgt0ap  10556  sqge0  10564  nnlesq  10591  expnbnd  10611  nn0opthlem2d  10667  facwordi  10686  filtinf  10737  hashunlem  10750  zfz1isolemiso  10785  cjmulge0  10864  resqrexlemover  10985  resqrexlemdec  10986  resqrexlemlo  10988  resqrexlemcalc3  10991  resqrexlemcvg  10994  resqrexlemoverl  10996  resqrexlemglsq  10997  resqrexlemga  10998  absge0  11035  amgm2  11093  maxle1  11186  bdtrilem  11213  xrmaxifle  11220  xrmaxiflemlub  11222  xrmaxiflemval  11224  xrmax1sup  11227  xrmaxltsup  11232  xrmaxadd  11235  xrbdtri  11250  reccn2ap  11287  climle  11308  climserle  11319  isumclim2  11396  isumclim3  11397  isumge0  11404  fsumlessfi  11434  expcnvap0  11476  expcnvre  11477  explecnv  11479  absltap  11483  cvgratnnlembern  11497  cvgratnnlemnexp  11498  cvgratnnlemmn  11499  cvgratnnlemabsle  11501  cvgratnnlemfm  11503  cvgratnnlemrate  11504  mertenslemi1  11509  mertenslem2  11510  clim2divap  11514  prodmodclem3  11549  efcvg  11640  ege2le3  11645  efaddlem  11648  eftlub  11664  effsumlt  11666  ef01bndlem  11730  sin02gt0  11737  eirrap  11751  iddvdsexp  11788  dvdsadd  11809  dvdsfac  11831  dvdsmod  11833  omoe  11866  divalglemnn  11888  divalglemnqt  11890  flodddiv4t2lthalf  11907  dvdslegcd  11930  dfgcd3  11976  dvdssqim  11990  dvdsmulgcd  11991  nn0seqcvgd  12006  dvdslcm  12034  lcmgcdlem  12042  mulgcddvds  12059  qredeq  12061  cncongr2  12069  sqnprm  12101  isprm6  12112  sqpweven  12140  znege1  12143  sqrt2irrap  12145  nonsq  12172  hashdvds  12186  prmdiv  12200  odzdvds  12210  pythagtriplem4  12233  pcpre1  12257  pcdvdsb  12284  pcz  12296  pcprmpw2  12297  pcaddlem  12303  pcadd  12304  pcmpt  12306  pcmptdvds  12308  fldivp1  12311  pcfaclem  12312  pockthlem  12319  4sqlem6  12346  4sqlem8  12348  ennnfonelemkh  12378  nninfdclemp1  12416  psmetxrge0  13383  isxmet2d  13399  mettri  13424  xmettri3  13425  mettri3  13426  xblss2ps  13455  blss2ps  13457  blss2  13458  blssps  13478  blss  13479  xmetxp  13558  ivthdec  13673  sin0pilem1  13753  sinq12gt0  13802  tangtx  13810  cosordlem  13821  cosq34lt1  13822  logdivlti  13853  logbgcd1irrap  13939  lgsdilem2  13988  2sqlem3  14004  2sqlem8  14010  cvgcmp2nlemabs  14321  trilpolemclim  14325  trilpolemeq1  14329  apdifflemf  14335  apdifflemr  14336  nconstwlpolemgt0  14352