Theorem resdvopclptsd

Description: Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	resdvopclptsd.1	$$⊢\phi \to \frac{d\left(x\in ℂ⟼A\right)}{d_{ℂ}x}=\left(x\in ℂ⟼B\right)$$
	resdvopclptsd.2	$$⊢\left(\phi \wedge x\in ℂ\right)\to A\in ℂ$$
	resdvopclptsd.3	$$⊢\left(\phi \wedge x\in ℂ\right)\to B\in ℂ$$
Assertion	resdvopclptsd	$$⊢\phi \to \frac{d\left(x\in \left[0,1\right]⟼A\right)}{d_{ℝ}x}=\left(x\in \left(0,1\right)⟼B\right)$$

Proof

Step	Hyp	Ref	Expression
1		resdvopclptsd.1	$$⊢\phi \to \frac{d\left(x\in ℂ⟼A\right)}{d_{ℂ}x}=\left(x\in ℂ⟼B\right)$$
2		resdvopclptsd.2	$$⊢\left(\phi \wedge x\in ℂ\right)\to A\in ℂ$$
3		resdvopclptsd.3	$$⊢\left(\phi \wedge x\in ℂ\right)\to B\in ℂ$$
4		eqid	$$⊢\left(x\in ℂ⟼A\right)=\left(x\in ℂ⟼A\right)$$
5		0red	$$⊢\phi \to 0\in ℝ$$
6		1red	$$⊢\phi \to 1\in ℝ$$
7	4 2 1 3 5 6	dvmptresicc	$$⊢\phi \to \frac{d\left(x\in \left[0,1\right]⟼A\right)}{d_{ℝ}x}=\left(x\in \left(0,1\right)⟼B\right)$$