Theorem elsetpreimafvrab

Description: An element of the preimage of a function value expressed as a restricted class abstraction. (Contributed by AV, 9-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2	1	elsetpreimafvbi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
3		fveqeq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) )
4	3	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) } ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) )
5	2 4	bitr4di	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑦 ∈ 𝑆 ↔ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) } ) )
6	5	eqrdv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → 𝑆 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) } )