Theorem dff2

Description: Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007)

	Ref	Expression
Assertion	dff2	$$⊢F:A⟶B\leftrightarrow \left(FFnA\wedge F\subseteq A\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ffn	$$⊢F:A⟶B\to FFnA$$
2		fssxp	$$⊢F:A⟶B\to F\subseteq A\times B$$
3	1 2	jca	$$⊢F:A⟶B\to \left(FFnA\wedge F\subseteq A\times B\right)$$
4		rnss	$$⊢F\subseteq A\times B\to \mathrm{ran}F\subseteq \mathrm{ran}\left(A\times B\right)$$
5		rnxpss	$$⊢\mathrm{ran}\left(A\times B\right)\subseteq B$$
6	4 5	sstrdi	$$⊢F\subseteq A\times B\to \mathrm{ran}F\subseteq B$$
7	6	anim2i	$$⊢\left(FFnA\wedge F\subseteq A\times B\right)\to \left(FFnA\wedge \mathrm{ran}F\subseteq B\right)$$
8		df-f	$$⊢F:A⟶B\leftrightarrow \left(FFnA\wedge \mathrm{ran}F\subseteq B\right)$$
9	7 8	sylibr	$$⊢\left(FFnA\wedge F\subseteq A\times B\right)\to F:A⟶B$$
10	3 9	impbii	$$⊢F:A⟶B\leftrightarrow \left(FFnA\wedge F\subseteq A\times B\right)$$