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  7901  ltexprlemopl  7969  recexprlemloc  7999  cauappcvgprlemopl  8014  cauappcvgprlemladdfu  8022  cauappcvgprlem1  8027  caucvgprlemopl  8037  caucvgprlemladdfu  8045  caucvgprprlemopl  8065  caucvgprprlemexbt  8074  mulgt0sr  8146  archsr  8150  caucvgsrlemoffgt1  8167  suplocsrlemb  8174  suplocsrlem  8176  mulap0r  8946  prodgt0  9185  div4p1lem1div2  9564  mul2lt0rgt0  10172  xnn0dcle  10215  xnn0letri  10216  xleadd1a  10286  xltadd1  10289  xlt2add  10293  xposdif  10295  xlesubadd  10296  xleaddadd  10300  uzsubsubfz  10463  fzctr  10551  subfzo0  10672  exbtwnzlemstep  10693  exbtwnzlemex  10695  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnxr  10703  xqltnle  10713  fldiv4lem1div2uz2  10756  ceilqge  10762  modqge0  10784  modqlt  10785  modqid  10801  m1modge3gt1  10823  modaddmodup  10839  addmodlteq  10850  ser3mono  10939  seqf1oglem1  10971  seqf1oglem2  10972  ser3ge0  10988  ser3le  10989  leexp1a  11046  sqgt0ap  11060  sqge0  11068  nnlesq  11095  expnbnd  11116  nn0sqdc  11162  nn0opthlem2d  11175  facwordi  11194  bcm1n  11223  filtinf  11246  hashunlem  11260  zfz1isolemiso  11307  cats1fvd  11554  cjmulge0  11670  resqrexlemover  11792  resqrexlemdec  11793  resqrexlemlo  11795  resqrexlemcalc3  11798  resqrexlemcvg  11801  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemga  11805  absge0  11842  amgm2  11901  maxle1  11994  bdtrilem  12024  xrmaxifle  12031  xrmaxiflemlub  12033  xrmaxiflemval  12035  xrmax1sup  12038  xrmaxltsup  12043  xrmaxadd  12046  xrbdtri  12061  reccn2ap  12098  climle  12119  climserle  12130  isumclim2  12208  isumclim3  12209  isumge0  12216  fsumlessfi  12246  expcnvap0  12288  expcnvre  12289  explecnv  12291  absltap  12295  cvgratnnlembern  12309  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemabsle  12313  cvgratnnlemfm  12315  cvgratnnlemrate  12316  mertenslemi1  12321  mertenslem2  12322  clim2divap  12326  prodmodclem3  12361  efcvg  12452  ege2le3  12457  efaddlem  12460  eftlub  12476  effsumlt  12478  ef01bndlem  12542  sin02gt0  12550  eirrap  12564  iddvdsexp  12601  dvdsadd  12622  dvdsfac  12646  dvdsmod  12648  3dvds  12650  omoe  12682  divalglemnn  12704  divalglemnqt  12706  flodddiv4t2lthalf  12725  bitsfzo  12741  bitsmod  12742  bitscmp  12744  bitsinv1lem  12747  dvdslegcd  12760  dfgcd3  12806  dvdssqim  12820  dvdsmulgcd  12821  nn0seqcvgd  12838  dvdslcm  12866  lcmgcdlem  12874  mulgcddvds  12891  qredeq  12893  cncongr2  12901  sqnprm  12934  isprm6  12945  sqpweven  12974  znege1  12977  sqrt2irrap  12979  nonsq  13006  hashdvds  13022  prmdiv  13036  odzdvds  13047  pythagtriplem4  13070  pcpre1  13094  pcdvdsb  13122  pcz  13134  pcprmpw2  13135  pcaddlem  13141  pcadd  13142  pcadd2  13143  pcmpt  13145  pcmptdvds  13147  fldivp1  13150  pcfaclem  13151  pockthlem  13158  4sqlem6  13185  4sqlem8  13187  4sqexercise1  13200  4sqexercise2  13201  4sqlemsdc  13202  4sqlem11  13203  4sqlem12  13204  4sqlem14  13206  4sqlem16  13208  ballotfilemsgt1  13306  ballotfilemsel1i  13308  ennnfonelemkh  13355  nninfdclemp1  13393  eqgen  14083  dvdsrmul1  14493  unitmulclb  14505  subrguss  14628  znidom  15076  znunit  15078  mplsubgfilemcl  15181  psmetxrge0  15524  isxmet2d  15540  mettri  15565  xmettri3  15566  mettri3  15567  xblss2ps  15596  blss2ps  15598  blss2  15599  blssps  15619  blss  15620  xmetxp  15699  ivthdec  15836  ivthreinc  15837  hoverb  15840  hovergt0  15842  sin0pilem1  15974  sinq12gt0  16023  tangtx  16031  cosordlem  16042  cosq34lt1  16043  logdivlti  16075  logbgcd1irrap  16167  birthdaylem3  16188  chtqge0  16208  chtublem  16256  perfectlem1  16260  bcmax  16266  bposlem1  16272  bposlem2  16273  bposlem5  16276  bposlem6  16277  bposlem7  16278  lgsdilem2  16321  gausslemma2dlem1f1o  16345  lgsquadlem1  16362  2lgsoddprmlem2  16391  2sqlem3  16402  2sqlem8  16408  usgrsizedgen  16620  cvgcmp2nlemabs  17247  trilpolemclim  17252  trilpolemeq1  17256  apdifflemf  17262  apdifflemr  17263  nconstwlpolemgt0  17281