Theorem eqbrtrd 4153

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrd.1	|- ( ph -> A = B )
eqbrtrd.2	|- ( ph -> B R C )

Assertion

Ref	Expression
eqbrtrd	|- ( ph -> A R C )

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 |- ( ph -> B R C )
2		eqbrtrd.1	. . 3 |- ( ph -> A = B )
3	2	breq1d 4141	. 2 |- ( ph -> ( A R C <-> B R C ) )
4	1, 3	mpbird 167	1 |- ( ph -> A R C )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   class class class wbr 4131

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 4132

This theorem is used by:  eqbrtrrd  4155  dif1en  7187  ccfunen  7636  prarloclemcalc  7875  ltexprlemopu  7976  recexprlemloc  8004  caucvgprprlemloccalc  8057  suplocsrlem  8181  axpre-suploclemres  8274  lesub3d  8898  mulle0r  9282  lbinfle  9288  divge1  10141  ltesubnnd  10187  xltnegi  10254  xleadd1a  10292  xltadd1  10295  xlt2add  10299  xposdif  10301  xleaddadd  10306  lincmble  10423  ubmelm1fzo  10661  infssfzledc  10687  zsupssdc  10690  qbtwnrelemcalc  10707  qbtwnxr  10709  ceiqm1l  10769  ceilqm1lt  10770  ceilqle  10772  modqlt  10791  modqeqmodmin  10852  addmodlteq  10856  seqf1oglem1  10977  exp3vallem  10998  bernneq  11119  nn0ltexp2  11169  faclbnd2  11202  sshashneg  11303  ccatsymb  11392  ccatrn  11399  sq01  11682  resqrexlemdec  11799  resqrexlemcalc2  11803  resqrexlemglsq  11810  resqrexlemga  11811  abslt  11877  amgm2  11907  icodiamlt  11969  maxabsle  11993  maxltsup  12007  minmax  12020  min1inf  12022  min2inf  12023  bdtrilem  12030  xrmaxltsup  12049  xrmaxaddlem  12051  xrmaxadd  12052  xrminmax  12056  xrmin1inf  12058  xrmin2inf  12059  climconst  12081  serclim0  12096  mulcn2  12103  reccn2ap  12104  iserex  12130  climlec2  12132  iserge0  12134  climcau  12138  climcvg1nlem  12140  fsumabs  12257  iserabs  12267  isumlessdc  12288  divcnv  12289  expcnvre  12295  absgtap  12302  georeclim  12305  cvgratnnlembern  12315  cvgratnnlemsumlt  12320  cvgratnnlemfm  12321  cvgratnnlemrate  12322  mertenslemub  12326  mertenslemi1  12327  prodfclim1  12336  prodfap0  12337  efcvgfsum  12459  eftlub  12482  eflegeo  12493  tanval3ap  12506  tannegap  12520  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  cos01gt0  12555  bitsfzolem  12746  bitsfzo  12747  bitsinv1lem  12753  mulgcd  12818  nnminle  12837  eucalglt  12860  lcmledvds  12873  mulgcddvds  12897  prmind2  12923  isprm5lem  12945  pwbdvdslemn  12969  pwbdvdseulemle  12971  nnmaxpwlemdvds  12974  sqrt2irrap  12985  divdenle  13002  nonsq  13012  pythagtriplem4  13076  pclem0  13094  pcpremul  13101  pczdvds  13122  pcprmpw2  13141  qexpz  13160  4sqlem10  13195  ballotfilemimin  13307  ballotfilemsel1i  13314  ballotfilemro  13324  ennnfonelemkh  13361  triv1nsgd  14080  qusgrp  14094  gzsumsplit0  14238  prdsbaslemss  14281  bl2in  15629  xblcntrps  15639  xblcntr  15640  ssblps  15651  ssbl  15652  blssps  15653  blss  15654  xmetxp  15733  mulc1cncf  15815  cncfmptc  15822  mulcncflem  15833  ivthinclemlopn  15862  ivthinclemuopn  15864  ivthdec  15870  ivthreinc  15871  hovera  15873  hoverlt1  15875  limcimolemlt  15890  cnplimclemle  15894  cnplimclemr  15895  limccnp2lem  15902  dveflem  15952  reeff1olem  15997  reeff1oleme  15998  tangtx  16065  cosq34lt1  16078  logdivlti  16111  cxpap0  16137  rpabscxpbnd  16175  birthdaylem3  16227  pellexlem2  16230  ppiqp1le  16267  ppiqltx  16281  ppiqub  16293  chtublem  16295  mersenne  16297  bcmono  16304  bcmax  16305  bposlem2  16312  bposlem5  16315  lgslem3  16326  gausslemma2dlem1a  16382  lgsquadlem1  16401  lgsquadlem2  16402  2lgslem1c  16414  subumgredg2en  16717  qdencn  17278  cvgcmp2nlemabs  17287  trilpolemclim  17292  trilpolemisumle  17294  trilpolemeq1  17296  apdifflemf  17302  apdifflemr  17303