Theorem fnex

Description: If the domain of a function is a set, the function is a set. Theorem 6.16(1) of TakeutiZaring p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg . See fnexALT for alternate proof. (Contributed by NM, 14-Aug-1994) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Assertion	fnex	|- ( ( F Fn A /\ A e. B ) -> F e. _V )

Proof

Step	Hyp	Ref	Expression
1		fnrel	|- ( F Fn A -> Rel F )
2		df-fn	|- ( F Fn A <-> ( Fun F /\ dom F = A ) )
3		eleq1a	|- ( A e. B -> ( dom F = A -> dom F e. B ) )
4	3	impcom	|- ( ( dom F = A /\ A e. B ) -> dom F e. B )
5		resfunexg	|- ( ( Fun F /\ dom F e. B ) -> ( F |` dom F ) e. _V )
6	4 5	sylan2	|- ( ( Fun F /\ ( dom F = A /\ A e. B ) ) -> ( F |` dom F ) e. _V )
7	6	anassrs	|- ( ( ( Fun F /\ dom F = A ) /\ A e. B ) -> ( F |` dom F ) e. _V )
8	2 7	sylanb	|- ( ( F Fn A /\ A e. B ) -> ( F |` dom F ) e. _V )
9		resdm	|- ( Rel F -> ( F |` dom F ) = F )
10	9	eleq1d	|- ( Rel F -> ( ( F |` dom F ) e. _V <-> F e. _V ) )
11	10	biimpa	|- ( ( Rel F /\ ( F |` dom F ) e. _V ) -> F e. _V )
12	1 8 11	syl2an2r	|- ( ( F Fn A /\ A e. B ) -> F e. _V )