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	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
Assertion	setpreimafvex	|- ( A e. V -> P e. _V )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2		abrexexg	|- ( A e. V -> { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } e. _V )
3	1 2	eqeltrid	|- ( A e. V -> P e. _V )