Theorem sloteq

Description: Equality theorem for the Slot construction. The converse holds if A (or B ) is a set. (Contributed by BJ, 27-Dec-2021)

	Ref	Expression
Assertion	sloteq	$$⊢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$$