Theorem bj-evaleq

Description: Equality theorem for the Slot construction. This is currently a duplicate of sloteq but may diverge from it if/when a token Eval is introduced for evaluation in order to separate it from Slot and any of its possible modifications. (Contributed by BJ, 27-Dec-2021) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-evaleq	$$⊢A=B\to \mathrm{Slot}A=\mathrm{Slot}B$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=B\to f\left(A\right)=f\left(B\right)$$
2	1	mpteq2dv	$$⊢A=B\to \left(f\in \mathrm{V}⟼f\left(A\right)\right)=\left(f\in \mathrm{V}⟼f\left(B\right)\right)$$
3		df-slot	$$⊢\mathrm{Slot}A=\left(f\in \mathrm{V}⟼f\left(A\right)\right)$$
4		df-slot	$$⊢\mathrm{Slot}B=\left(f\in \mathrm{V}⟼f\left(B\right)\right)$$
5	2 3 4	3eqtr4g	$$⊢A=B\to \mathrm{Slot}A=\mathrm{Slot}B$$