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  7189  ccfunen  7636  prarloclemcalc  7875  ltexprlemopu  7976  recexprlemloc  8004  caucvgprprlemloccalc  8057  suplocsrlem  8181  axpre-suploclemres  8274  lesub3d  8898  mulle0r  9282  lbinfle  9288  divge1  10140  ltesubnnd  10186  xltnegi  10253  xleadd1a  10291  xltadd1  10294  xlt2add  10298  xposdif  10300  xleaddadd  10305  lincmble  10422  ubmelm1fzo  10660  infssfzledc  10686  zsupssdc  10689  qbtwnrelemcalc  10706  qbtwnxr  10708  ceiqm1l  10768  ceilqm1lt  10769  ceilqle  10771  modqlt  10790  modqeqmodmin  10851  addmodlteq  10855  seqf1oglem1  10976  exp3vallem  10997  bernneq  11118  nn0ltexp2  11168  faclbnd2  11201  sshashneg  11302  ccatsymb  11391  ccatrn  11398  sq01  11681  resqrexlemdec  11798  resqrexlemcalc2  11802  resqrexlemglsq  11809  resqrexlemga  11810  abslt  11876  amgm2  11906  icodiamlt  11968  maxabsle  11992  maxltsup  12006  minmax  12019  min1inf  12021  min2inf  12022  bdtrilem  12029  xrmaxltsup  12048  xrmaxaddlem  12050  xrmaxadd  12051  xrminmax  12055  xrmin1inf  12057  xrmin2inf  12058  climconst  12080  serclim0  12095  mulcn2  12102  reccn2ap  12103  iserex  12129  climlec2  12131  iserge0  12133  climcau  12137  climcvg1nlem  12139  fsumabs  12256  iserabs  12266  isumlessdc  12287  divcnv  12288  expcnvre  12294  absgtap  12301  georeclim  12304  cvgratnnlembern  12314  cvgratnnlemsumlt  12319  cvgratnnlemfm  12320  cvgratnnlemrate  12321  mertenslemub  12325  mertenslemi1  12326  prodfclim1  12335  prodfap0  12336  efcvgfsum  12458  eftlub  12481  eflegeo  12492  tanval3ap  12505  tannegap  12519  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  cos01gt0  12554  bitsfzolem  12745  bitsfzo  12746  bitsinv1lem  12752  mulgcd  12817  nnminle  12836  eucalglt  12859  lcmledvds  12872  mulgcddvds  12896  prmind2  12922  isprm5lem  12944  pwbdvdslemn  12968  pwbdvdseulemle  12970  nnmaxpwlemdvds  12973  sqrt2irrap  12984  divdenle  13001  nonsq  13011  pythagtriplem4  13075  pclem0  13093  pcpremul  13100  pczdvds  13121  pcprmpw2  13140  qexpz  13159  4sqlem10  13194  ballotfilemimin  13306  ballotfilemsel1i  13313  ballotfilemro  13323  ennnfonelemkh  13360  triv1nsgd  14079  qusgrp  14093  gzsumsplit0  14237  prdsbaslemss  14280  bl2in  15646  xblcntrps  15656  xblcntr  15657  ssblps  15668  ssbl  15669  blssps  15670  blss  15671  xmetxp  15750  mulc1cncf  15832  cncfmptc  15839  mulcncflem  15850  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthdec  15887  ivthreinc  15888  hovera  15890  hoverlt1  15892  limcimolemlt  15907  cnplimclemle  15911  cnplimclemr  15912  limccnp2lem  15919  dveflem  15969  reeff1olem  16014  reeff1oleme  16015  tangtx  16082  cosq34lt1  16095  logdivlti  16128  cxpap0  16154  rpabscxpbnd  16192  birthdaylem3  16244  pellexlem2  16247  ppiqp1le  16284  ppiqltx  16298  ppiqub  16310  chtublem  16312  mersenne  16314  bcmono  16321  bcmax  16322  bposlem2  16329  bposlem5  16332  lgslem3  16343  gausslemma2dlem1a  16399  lgsquadlem1  16418  lgsquadlem2  16419  2lgslem1c  16431  subumgredg2en  16734  qdencn  17295  cvgcmp2nlemabs  17304  trilpolemclim  17309  trilpolemisumle  17311  trilpolemeq1  17313  apdifflemf  17319  apdifflemr  17320