Theorem elfv2ex

Description: If a function value of a function value has a member, then the first argument is a set. (Contributed by AV, 8-Apr-2021)

	Ref	Expression
Assertion	elfv2ex	$$⊢A\in F\left(B\right)\left(C\right)\to B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ax-1	$$⊢B\in \mathrm{V}\to \left(A\in F\left(B\right)\left(C\right)\to B\in \mathrm{V}\right)$$
2		fv2prc	$$⊢\neg B\in \mathrm{V}\to F\left(B\right)\left(C\right)=\varnothing$$
3	2	eleq2d	$$⊢\neg B\in \mathrm{V}\to \left(A\in F\left(B\right)\left(C\right)\leftrightarrow A\in \varnothing \right)$$
4		noel	$$⊢\neg A\in \varnothing$$
5	4	pm2.21i	$$⊢A\in \varnothing \to B\in \mathrm{V}$$
6	3 5	syl6bi	$$⊢\neg B\in \mathrm{V}\to \left(A\in F\left(B\right)\left(C\right)\to B\in \mathrm{V}\right)$$
7	1 6	pm2.61i	$$⊢A\in F\left(B\right)\left(C\right)\to B\in \mathrm{V}$$