Theorem setpreimafvex

Description: The class P of all preimages of function values is a set. (Contributed by AV, 10-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
Assertion	setpreimafvex	⊢ ( 𝐴 ∈ 𝑉 → 𝑃 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		abrexexg	⊢ ( 𝐴 ∈ 𝑉 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } ∈ V )
3	1 2	eqeltrid	⊢ ( 𝐴 ∈ 𝑉 → 𝑃 ∈ V )