Theorem eqfvelsetpreimafv

Description: If an element of the domain of the function has the same function value as an element of the preimage of a function value, then it is an element of the same preimage. (Contributed by AV, 9-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
Assertion	eqfvelsetpreimafv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) → 𝑌 ∈ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2	1	elsetpreimafvbi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
3	2	biimprd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) → 𝑌 ∈ 𝑆 ) )