Theorem elfvexd

Description: If a function value has a member, then its argument is a set. Deduction form of elfvex . (An artifact of our function value definition.) (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypothesis	elfvexd.1	|- ( ph -> A e. ( B ` C ) )
Assertion	elfvexd	|- ( ph -> C e. _V )

Proof

Step	Hyp	Ref	Expression
1		elfvexd.1	|- ( ph -> A e. ( B ` C ) )
2		elfvex	|- ( A e. ( B ` C ) -> C e. _V )
3	1 2	syl	|- ( ph -> C e. _V )