Theorem breqtrrd 4158

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  frirrg  4495  fidcen  7203  unsnfidcex  7227  unsnfidcel  7228  addlocprlemeq  7900  ltexprlemopl  7968  recexprlemloc  7998  cauappcvgprlemopl  8013  cauappcvgprlemladdfu  8021  cauappcvgprlem1  8026  caucvgprlemopl  8036  caucvgprlemladdfu  8044  caucvgprprlemopl  8064  caucvgprprlemexbt  8073  mulgt0sr  8145  archsr  8149  caucvgsrlemoffgt1  8166  suplocsrlemb  8173  suplocsrlem  8175  mulap0r  8945  prodgt0  9184  div4p1lem1div2  9563  mul2lt0rgt0  10171  xnn0dcle  10214  xnn0letri  10215  xleadd1a  10285  xltadd1  10288  xlt2add  10292  xposdif  10294  xlesubadd  10295  xleaddadd  10299  uzsubsubfz  10462  fzctr  10550  subfzo0  10671  exbtwnzlemstep  10692  exbtwnzlemex  10694  rebtwn2zlemstep  10697  rebtwn2z  10699  qbtwnxr  10702  xqltnle  10712  fldiv4lem1div2uz2  10754  ceilqge  10760  modqge0  10782  modqlt  10783  modqid  10799  m1modge3gt1  10821  modaddmodup  10837  addmodlteq  10848  ser3mono  10937  seqf1oglem1  10969  seqf1oglem2  10970  ser3ge0  10986  ser3le  10987  leexp1a  11044  sqgt0ap  11058  sqge0  11066  nnlesq  11093  expnbnd  11114  nn0sqdc  11160  nn0opthlem2d  11173  facwordi  11192  bcm1n  11221  filtinf  11244  hashunlem  11258  zfz1isolemiso  11305  cats1fvd  11552  cjmulge0  11668  resqrexlemover  11790  resqrexlemdec  11791  resqrexlemlo  11793  resqrexlemcalc3  11796  resqrexlemcvg  11799  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemga  11803  absge0  11840  amgm2  11899  maxle1  11992  bdtrilem  12021  xrmaxifle  12028  xrmaxiflemlub  12030  xrmaxiflemval  12032  xrmax1sup  12035  xrmaxltsup  12040  xrmaxadd  12043  xrbdtri  12058  reccn2ap  12095  climle  12116  climserle  12127  isumclim2  12205  isumclim3  12206  isumge0  12213  fsumlessfi  12243  expcnvap0  12285  expcnvre  12286  explecnv  12288  absltap  12292  cvgratnnlembern  12306  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemabsle  12310  cvgratnnlemfm  12312  cvgratnnlemrate  12313  mertenslemi1  12318  mertenslem2  12319  clim2divap  12323  prodmodclem3  12358  efcvg  12449  ege2le3  12454  efaddlem  12457  eftlub  12473  effsumlt  12475  ef01bndlem  12539  sin02gt0  12547  eirrap  12561  iddvdsexp  12598  dvdsadd  12619  dvdsfac  12643  dvdsmod  12645  3dvds  12647  omoe  12679  divalglemnn  12701  divalglemnqt  12703  flodddiv4t2lthalf  12722  bitsfzo  12738  bitsmod  12739  bitscmp  12741  bitsinv1lem  12744  dvdslegcd  12757  dfgcd3  12803  dvdssqim  12817  dvdsmulgcd  12818  nn0seqcvgd  12835  dvdslcm  12863  lcmgcdlem  12871  mulgcddvds  12888  qredeq  12890  cncongr2  12898  sqnprm  12931  isprm6  12942  sqpweven  12971  znege1  12974  sqrt2irrap  12976  nonsq  13003  hashdvds  13019  prmdiv  13033  odzdvds  13044  pythagtriplem4  13067  pcpre1  13091  pcdvdsb  13119  pcz  13131  pcprmpw2  13132  pcaddlem  13138  pcadd  13139  pcadd2  13140  pcmpt  13142  pcmptdvds  13144  fldivp1  13147  pcfaclem  13148  pockthlem  13155  4sqlem6  13182  4sqlem8  13184  4sqexercise1  13197  4sqexercise2  13198  4sqlemsdc  13199  4sqlem11  13200  4sqlem12  13201  4sqlem14  13203  4sqlem16  13205  ballotfilemsgt1  13303  ballotfilemsel1i  13305  ennnfonelemkh  13352  nninfdclemp1  13390  eqgen  14079  dvdsrmul1  14458  unitmulclb  14470  subrguss  14593  znidom  15041  znunit  15043  mplsubgfilemcl  15139  psmetxrge0  15482  isxmet2d  15498  mettri  15523  xmettri3  15524  mettri3  15525  xblss2ps  15554  blss2ps  15556  blss2  15557  blssps  15577  blss  15578  xmetxp  15657  ivthdec  15794  ivthreinc  15795  hoverb  15798  hovergt0  15800  sin0pilem1  15932  sinq12gt0  15981  tangtx  15989  cosordlem  16000  cosq34lt1  16001  logdivlti  16033  logbgcd1irrap  16125  birthdaylem3  16146  perfectlem1  16197  bcmax  16203  bposlem1  16209  bposlem2  16210  bposlem5  16213  lgsdilem2  16253  gausslemma2dlem1f1o  16277  lgsquadlem1  16294  2lgsoddprmlem2  16323  2sqlem3  16334  2sqlem8  16340  usgrsizedgen  16552  cvgcmp2nlemabs  17179  trilpolemclim  17183  trilpolemeq1  17187  apdifflemf  17193  apdifflemr  17194  nconstwlpolemgt0  17212