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	⊢ ( 𝐸 ‘ ∅ ) = ∅
	fveqprc.y	⊢ 𝑌 = ( 𝐹 ‘ 𝑋 )
Assertion	fveqprc	⊢ ( ¬ 𝑋 ∈ V → ( 𝐸 ‘ 𝑋 ) = ( 𝐸 ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		fveqprc.e	⊢ ( 𝐸 ‘ ∅ ) = ∅
2		fveqprc.y	⊢ 𝑌 = ( 𝐹 ‘ 𝑋 )
3	1	eqcomi	⊢ ∅ = ( 𝐸 ‘ ∅ )
4		fvprc	⊢ ( ¬ 𝑋 ∈ V → ( 𝐸 ‘ 𝑋 ) = ∅ )
5		fvprc	⊢ ( ¬ 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = ∅ )
6	2 5	eqtrid	⊢ ( ¬ 𝑋 ∈ V → 𝑌 = ∅ )
7	6	fveq2d	⊢ ( ¬ 𝑋 ∈ V → ( 𝐸 ‘ 𝑌 ) = ( 𝐸 ‘ ∅ ) )
8	3 4 7	3eqtr4a	⊢ ( ¬ 𝑋 ∈ V → ( 𝐸 ‘ 𝑋 ) = ( 𝐸 ‘ 𝑌 ) )