Theorem breqtrrd 4142

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  frirrg  4476  fidcen  7169  unsnfidcex  7193  unsnfidcel  7194  addlocprlemeq  7864  ltexprlemopl  7932  recexprlemloc  7962  cauappcvgprlemopl  7977  cauappcvgprlemladdfu  7985  cauappcvgprlem1  7990  caucvgprlemopl  8000  caucvgprlemladdfu  8008  caucvgprprlemopl  8028  caucvgprprlemexbt  8037  mulgt0sr  8109  archsr  8113  caucvgsrlemoffgt1  8130  suplocsrlemb  8137  suplocsrlem  8139  mulap0r  8906  prodgt0  9143  div4p1lem1div2  9509  mul2lt0rgt0  10111  xnn0dcle  10154  xnn0letri  10155  xleadd1a  10225  xltadd1  10228  xlt2add  10232  xposdif  10234  xlesubadd  10235  xleaddadd  10239  uzsubsubfz  10401  fzctr  10489  subfzo0  10610  exbtwnzlemstep  10631  exbtwnzlemex  10633  rebtwn2zlemstep  10636  rebtwn2z  10638  qbtwnxr  10641  xqltnle  10651  fldiv4lem1div2uz2  10690  ceilqge  10696  modqge0  10718  modqlt  10719  modqid  10735  m1modge3gt1  10757  modaddmodup  10773  addmodlteq  10784  ser3mono  10873  seqf1oglem1  10905  seqf1oglem2  10906  ser3ge0  10922  ser3le  10923  leexp1a  10980  sqgt0ap  10994  sqge0  11002  nnlesq  11029  expnbnd  11050  nn0opthlem2d  11108  facwordi  11127  bcm1n  11156  filtinf  11179  hashunlem  11193  zfz1isolemiso  11236  cats1fvd  11483  cjmulge0  11599  resqrexlemover  11720  resqrexlemdec  11721  resqrexlemlo  11723  resqrexlemcalc3  11726  resqrexlemcvg  11729  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemga  11733  absge0  11770  amgm2  11828  maxle1  11921  bdtrilem  11949  xrmaxifle  11956  xrmaxiflemlub  11958  xrmaxiflemval  11960  xrmax1sup  11963  xrmaxltsup  11968  xrmaxadd  11971  xrbdtri  11986  reccn2ap  12023  climle  12044  climserle  12055  isumclim2  12133  isumclim3  12134  isumge0  12141  fsumlessfi  12171  expcnvap0  12213  expcnvre  12214  explecnv  12216  absltap  12220  cvgratnnlembern  12234  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemabsle  12238  cvgratnnlemfm  12240  cvgratnnlemrate  12241  mertenslemi1  12246  mertenslem2  12247  clim2divap  12251  prodmodclem3  12286  efcvg  12377  ege2le3  12382  efaddlem  12385  eftlub  12401  effsumlt  12403  ef01bndlem  12467  sin02gt0  12475  eirrap  12489  iddvdsexp  12526  dvdsadd  12547  dvdsfac  12571  dvdsmod  12573  3dvds  12575  omoe  12607  divalglemnn  12629  divalglemnqt  12631  flodddiv4t2lthalf  12650  bitsfzo  12666  bitsmod  12667  bitscmp  12669  bitsinv1lem  12672  dvdslegcd  12685  dfgcd3  12731  dvdssqim  12745  dvdsmulgcd  12746  nn0seqcvgd  12763  dvdslcm  12791  lcmgcdlem  12799  mulgcddvds  12816  qredeq  12818  cncongr2  12826  sqnprm  12858  isprm6  12869  sqpweven  12897  znege1  12900  sqrt2irrap  12902  nonsq  12929  hashdvds  12943  prmdiv  12957  odzdvds  12968  pythagtriplem4  12991  pcpre1  13015  pcdvdsb  13043  pcz  13055  pcprmpw2  13056  pcaddlem  13062  pcadd  13063  pcadd2  13064  pcmpt  13066  pcmptdvds  13068  fldivp1  13071  pcfaclem  13072  pockthlem  13079  4sqlem6  13106  4sqlem8  13108  4sqexercise1  13121  4sqexercise2  13122  4sqlemsdc  13123  4sqlem11  13124  4sqlem12  13125  4sqlem14  13127  4sqlem16  13129  ballotfilemsgt1  13198  ballotfilemsel1i  13200  ennnfonelemkh  13247  nninfdclemp1  13285  eqgen  13980  dvdsrmul1  14347  unitmulclb  14359  subrguss  14482  znidom  14931  znunit  14933  mplsubgfilemcl  14980  psmetxrge0  15323  isxmet2d  15339  mettri  15364  xmettri3  15365  mettri3  15366  xblss2ps  15395  blss2ps  15397  blss2  15398  blssps  15418  blss  15419  xmetxp  15498  ivthdec  15635  ivthreinc  15636  hoverb  15639  hovergt0  15641  sin0pilem1  15772  sinq12gt0  15821  tangtx  15829  cosordlem  15840  cosq34lt1  15841  logdivlti  15872  logbgcd1irrap  15961  perfectlem1  15993  lgsdilem2  16035  gausslemma2dlem1f1o  16059  lgsquadlem1  16076  2lgsoddprmlem2  16105  2sqlem3  16116  2sqlem8  16122  usgrsizedgen  16334  cvgcmp2nlemabs  16942  trilpolemclim  16946  trilpolemeq1  16950  apdifflemf  16956  apdifflemr  16957  nconstwlpolemgt0  16976