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 \land A \in B) \to F \in V$

Proof

Step	Hyp	Ref	Expression
1		fnrel	$⊢ F Fn A \to Rel F$
2		df-fn	$⊢ F Fn A \leftrightarrow (Fun F \land dom F = A)$
3		eleq1a	$⊢ A \in B \to (dom F = A \to dom F \in B)$
4	3	impcom	$⊢ (dom F = A \land A \in B) \to dom F \in B$
5		resfunexg	$⊢ (Fun F \land dom F \in B) \to {F ↾}_{dom F} \in V$
6	4 5	sylan2	$⊢ (Fun F \land (dom F = A \land A \in B)) \to {F ↾}_{dom F} \in V$
7	6	anassrs	$⊢ ((Fun F \land dom F = A) \land A \in B) \to {F ↾}_{dom F} \in V$
8	2 7	sylanb	$⊢ (F Fn A \land A \in B) \to {F ↾}_{dom F} \in V$
9		resdm	$⊢ Rel F \to {F ↾}_{dom F} = F$
10	9	eleq1d	$⊢ Rel F \to ({F ↾}_{dom F} \in V \leftrightarrow F \in V)$
11	10	biimpa	$⊢ (Rel F \land {F ↾}_{dom F} \in V) \to F \in V$
12	1 8 11	syl2an2r	$⊢ (F Fn A \land A \in B) \to F \in V$

Metamath Proof Explorer

Theorem fnex

Proof