Theorem preimafvsnel

Description: The preimage of a function value at X contains X . (Contributed by AV, 7-Mar-2024)

	Ref	Expression
Assertion	preimafvsnel	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
2		eqidd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
3		fniniseg	⊢ ( 𝐹 Fn 𝐴 → ( 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
4	3	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
5	1 2 4	mpbir2and	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) )