Theorem fveqprc

Description: Lemma for showing the equality of values for functions like slot extractors E at a proper class. Extracted from several former proofs of lemmas like zlmlem . (Contributed by AV, 31-Oct-2024)

	Ref	Expression
Hypotheses	fveqprc.e	$$⊢E\left(\varnothing \right)=\varnothing$$
	fveqprc.y	$$⊢Y=F\left(X\right)$$
Assertion	fveqprc	$$⊢\neg X\in \mathrm{V}\to E\left(X\right)=E\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveqprc.e	$$⊢E\left(\varnothing \right)=\varnothing$$
2		fveqprc.y	$$⊢Y=F\left(X\right)$$
3	1	eqcomi	$$⊢\varnothing =E\left(\varnothing \right)$$
4		fvprc	$$⊢\neg X\in \mathrm{V}\to E\left(X\right)=\varnothing$$
5		fvprc	$$⊢\neg X\in \mathrm{V}\to F\left(X\right)=\varnothing$$
6	2 5	eqtrid	$$⊢\neg X\in \mathrm{V}\to Y=\varnothing$$
7	6	fveq2d	$$⊢\neg X\in \mathrm{V}\to E\left(Y\right)=E\left(\varnothing \right)$$
8	3 4 7	3eqtr4a	$$⊢\neg X\in \mathrm{V}\to E\left(X\right)=E\left(Y\right)$$