Theorem oveqprc

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 resvlem . (Contributed by AV, 31-Oct-2024)

	Ref	Expression
Hypotheses	oveqprc.e	$$⊢E\left(\varnothing \right)=\varnothing$$
	oveqprc.z	$$⊢Z=XOY$$
	oveqprc.r	$$⊢\mathrm{Rel}\mathrm{dom}O$$
Assertion	oveqprc	$$⊢\neg X\in \mathrm{V}\to E\left(X\right)=E\left(Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveqprc.e	$$⊢E\left(\varnothing \right)=\varnothing$$
2		oveqprc.z	$$⊢Z=XOY$$
3		oveqprc.r	$$⊢\mathrm{Rel}\mathrm{dom}O$$
4	1	eqcomi	$$⊢\varnothing =E\left(\varnothing \right)$$
5		fvprc	$$⊢\neg X\in \mathrm{V}\to E\left(X\right)=\varnothing$$
6	3	ovprc1	$$⊢\neg X\in \mathrm{V}\to XOY=\varnothing$$
7	2 6	eqtrid	$$⊢\neg X\in \mathrm{V}\to Z=\varnothing$$
8	7	fveq2d	$$⊢\neg X\in \mathrm{V}\to E\left(Z\right)=E\left(\varnothing \right)$$
9	4 5 8	3eqtr4a	$$⊢\neg X\in \mathrm{V}\to E\left(X\right)=E\left(Z\right)$$