Theorem eqbrtrd 4052

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 4040	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 167	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031

This theorem is referenced by:  eqbrtrrd  4054  dif1en  6937  ccfunen  7326  prarloclemcalc  7564  ltexprlemopu  7665  recexprlemloc  7693  caucvgprprlemloccalc  7746  suplocsrlem  7870  axpre-suploclemres  7963  mulle0r  8965  lbinfle  8971  divge1  9792  xltnegi  9904  xleadd1a  9942  xltadd1  9945  xlt2add  9949  xposdif  9951  xleaddadd  9956  ubmelm1fzo  10296  qbtwnrelemcalc  10327  qbtwnxr  10329  ceiqm1l  10385  ceilqm1lt  10386  ceilqle  10388  modqlt  10407  modqeqmodmin  10468  addmodlteq  10472  seqf1oglem1  10593  exp3vallem  10614  bernneq  10734  nn0ltexp2  10783  faclbnd2  10816  resqrexlemdec  11158  resqrexlemcalc2  11162  resqrexlemglsq  11169  resqrexlemga  11170  abslt  11235  amgm2  11265  icodiamlt  11327  maxabsle  11351  maxltsup  11365  minmax  11376  min1inf  11378  min2inf  11379  bdtrilem  11385  xrmaxltsup  11404  xrmaxaddlem  11406  xrmaxadd  11407  xrminmax  11411  xrmin1inf  11413  xrmin2inf  11414  climconst  11436  serclim0  11451  mulcn2  11458  reccn2ap  11459  iserex  11485  climlec2  11487  iserge0  11489  climcau  11493  climcvg1nlem  11495  fsumabs  11611  iserabs  11621  isumlessdc  11642  divcnv  11643  expcnvre  11649  absgtap  11656  georeclim  11659  cvgratnnlembern  11669  cvgratnnlemsumlt  11674  cvgratnnlemfm  11675  cvgratnnlemrate  11676  mertenslemub  11680  mertenslemi1  11681  prodfclim1  11690  prodfap0  11691  efcvgfsum  11813  eftlub  11836  eflegeo  11847  tanval3ap  11860  tannegap  11874  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  cos01gt0  11909  zsupssdc  12094  mulgcd  12156  nnminle  12175  eucalglt  12198  lcmledvds  12211  mulgcddvds  12235  prmind2  12261  isprm5lem  12282  pw2dvdslemn  12306  pw2dvdseulemle  12308  oddpwdclemdvds  12311  sqrt2irrap  12321  divdenle  12338  nonsq  12348  pythagtriplem4  12409  pclem0  12427  pcpremul  12434  pczdvds  12455  pcprmpw2  12474  qexpz  12493  4sqlem10  12528  ennnfonelemkh  12572  triv1nsgd  13291  qusgrp  13305  bl2in  14582  xblcntrps  14592  xblcntr  14593  ssblps  14604  ssbl  14605  blssps  14606  blss  14607  xmetxp  14686  mulc1cncf  14768  cncfmptc  14775  mulcncflem  14786  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthdec  14823  ivthreinc  14824  hovera  14826  hoverlt1  14828  limcimolemlt  14843  cnplimclemle  14847  cnplimclemr  14848  limccnp2lem  14855  dveflem  14905  reeff1olem  14947  reeff1oleme  14948  tangtx  15014  cosq34lt1  15026  logdivlti  15057  cxpap0  15080  rpabscxpbnd  15114  lgslem3  15159  gausslemma2dlem1a  15215  lgsquadlem1  15234  lgsquadlem2  15235  2lgslem1c  15247  qdencn  15587  cvgcmp2nlemabs  15592  trilpolemclim  15596  trilpolemisumle  15598  trilpolemeq1  15600  apdifflemf  15606  apdifflemr  15607