Theorem fvelimabd

Description: Deduction form of fvelimab . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	fvelimabd.1	$$⊢\phi \to FFnA$$
	fvelimabd.2	$$⊢\phi \to B\subseteq A$$
Assertion	fvelimabd	$$⊢\phi \to \left(C\in F\left[B\right]\leftrightarrow \exists x\in BF\left(x\right)=C\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvelimabd.1	$$⊢\phi \to FFnA$$
2		fvelimabd.2	$$⊢\phi \to B\subseteq A$$
3		fvelimab	$$⊢\left(FFnA\wedge B\subseteq A\right)\to \left(C\in F\left[B\right]\leftrightarrow \exists x\in BF\left(x\right)=C\right)$$
4	1 2 3	syl2anc	$$⊢\phi \to \left(C\in F\left[B\right]\leftrightarrow \exists x\in BF\left(x\right)=C\right)$$