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	⊢ ( 𝐸 ‘ ∅ ) = ∅
	oveqprc.z	⊢ 𝑍 = ( 𝑋 𝑂 𝑌 )
	oveqprc.r	⊢ Rel dom 𝑂
Assertion	oveqprc	⊢ ( ¬ 𝑋 ∈ V → ( 𝐸 ‘ 𝑋 ) = ( 𝐸 ‘ 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		oveqprc.e	⊢ ( 𝐸 ‘ ∅ ) = ∅
2		oveqprc.z	⊢ 𝑍 = ( 𝑋 𝑂 𝑌 )
3		oveqprc.r	⊢ Rel dom 𝑂
4	1	eqcomi	⊢ ∅ = ( 𝐸 ‘ ∅ )
5		fvprc	⊢ ( ¬ 𝑋 ∈ V → ( 𝐸 ‘ 𝑋 ) = ∅ )
6	3	ovprc1	⊢ ( ¬ 𝑋 ∈ V → ( 𝑋 𝑂 𝑌 ) = ∅ )
7	2 6	eqtrid	⊢ ( ¬ 𝑋 ∈ V → 𝑍 = ∅ )
8	7	fveq2d	⊢ ( ¬ 𝑋 ∈ V → ( 𝐸 ‘ 𝑍 ) = ( 𝐸 ‘ ∅ ) )
9	4 5 8	3eqtr4a	⊢ ( ¬ 𝑋 ∈ V → ( 𝐸 ‘ 𝑋 ) = ( 𝐸 ‘ 𝑍 ) )