Theorem eqbrtrd 4152

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

Hypotheses

Ref	Expression
eqbrtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqbrtrd.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
eqbrtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 4140	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 167	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:  eqbrtrrd  4154  dif1en  7183  ccfunen  7631  prarloclemcalc  7870  ltexprlemopu  7971  recexprlemloc  7999  caucvgprprlemloccalc  8052  suplocsrlem  8176  axpre-suploclemres  8269  lesub3d  8893  mulle0r  9277  lbinfle  9283  divge1  10135  ltesubnnd  10181  xltnegi  10248  xleadd1a  10286  xltadd1  10289  xlt2add  10293  xposdif  10295  xleaddadd  10300  lincmble  10417  ubmelm1fzo  10655  infssfzledc  10681  zsupssdc  10684  qbtwnrelemcalc  10701  qbtwnxr  10703  ceiqm1l  10763  ceilqm1lt  10764  ceilqle  10766  modqlt  10785  modqeqmodmin  10846  addmodlteq  10850  seqf1oglem1  10971  exp3vallem  10992  bernneq  11113  nn0ltexp2  11163  faclbnd2  11196  sshashneg  11297  ccatsymb  11386  ccatrn  11393  sq01  11676  resqrexlemdec  11793  resqrexlemcalc2  11797  resqrexlemglsq  11804  resqrexlemga  11805  abslt  11871  amgm2  11901  icodiamlt  11963  maxabsle  11987  maxltsup  12001  minmax  12014  min1inf  12016  min2inf  12017  bdtrilem  12024  xrmaxltsup  12043  xrmaxaddlem  12045  xrmaxadd  12046  xrminmax  12050  xrmin1inf  12052  xrmin2inf  12053  climconst  12075  serclim0  12090  mulcn2  12097  reccn2ap  12098  iserex  12124  climlec2  12126  iserge0  12128  climcau  12132  climcvg1nlem  12134  fsumabs  12251  iserabs  12261  isumlessdc  12282  divcnv  12283  expcnvre  12289  absgtap  12296  georeclim  12299  cvgratnnlembern  12309  cvgratnnlemsumlt  12314  cvgratnnlemfm  12315  cvgratnnlemrate  12316  mertenslemub  12320  mertenslemi1  12321  prodfclim1  12330  prodfap0  12331  efcvgfsum  12453  eftlub  12476  eflegeo  12487  tanval3ap  12500  tannegap  12514  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  cos01gt0  12549  bitsfzolem  12740  bitsfzo  12741  bitsinv1lem  12747  mulgcd  12812  nnminle  12831  eucalglt  12854  lcmledvds  12867  mulgcddvds  12891  prmind2  12917  isprm5lem  12939  pwbdvdslemn  12963  pwbdvdseulemle  12965  nnmaxpwlemdvds  12968  sqrt2irrap  12979  divdenle  12996  nonsq  13006  pythagtriplem4  13070  pclem0  13088  pcpremul  13095  pczdvds  13116  pcprmpw2  13135  qexpz  13154  4sqlem10  13189  ballotfilemimin  13301  ballotfilemsel1i  13308  ballotfilemro  13318  ennnfonelemkh  13355  triv1nsgd  14074  qusgrp  14088  gzsumsplit0  14232  prdsbaslemss  14258  bl2in  15595  xblcntrps  15605  xblcntr  15606  ssblps  15617  ssbl  15618  blssps  15619  blss  15620  xmetxp  15699  mulc1cncf  15781  cncfmptc  15788  mulcncflem  15799  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthdec  15836  ivthreinc  15837  hovera  15839  hoverlt1  15841  limcimolemlt  15856  cnplimclemle  15860  cnplimclemr  15861  limccnp2lem  15868  dveflem  15918  reeff1olem  15963  reeff1oleme  15964  tangtx  16031  cosq34lt1  16043  logdivlti  16075  cxpap0  16101  rpabscxpbnd  16137  birthdaylem3  16188  pellexlem2  16191  ppiqp1le  16228  ppiqltx  16242  ppiqub  16254  chtublem  16256  mersenne  16258  bcmono  16265  bcmax  16266  bposlem2  16273  bposlem5  16276  lgslem3  16287  gausslemma2dlem1a  16343  lgsquadlem1  16362  lgsquadlem2  16363  2lgslem1c  16375  subumgredg2en  16678  qdencn  17238  cvgcmp2nlemabs  17247  trilpolemclim  17252  trilpolemisumle  17254  trilpolemeq1  17256  apdifflemf  17262  apdifflemr  17263