Theorem elsetpreimafvb

Description: The characterization of an element of the class P of all preimages of function values. (Contributed by AV, 10-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
Assertion	elsetpreimafvb	|- ( S e. V -> ( S e. P <-> E. x e. A S = ( `' F " { ( F ` x ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2	1	eleq2i	|- ( S e. P <-> S e. { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } )
3		eqeq1	|- ( z = S -> ( z = ( `' F " { ( F ` x ) } ) <-> S = ( `' F " { ( F ` x ) } ) ) )
4	3	rexbidv	|- ( z = S -> ( E. x e. A z = ( `' F " { ( F ` x ) } ) <-> E. x e. A S = ( `' F " { ( F ` x ) } ) ) )
5	4	elabg	|- ( S e. V -> ( S e. { z | E. x e. A z = ( `' F " { ( F ` x ) } ) } <-> E. x e. A S = ( `' F " { ( F ` x ) } ) ) )
6	2 5	bitrid	|- ( S e. V -> ( S e. P <-> E. x e. A S = ( `' F " { ( F ` x ) } ) ) )