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	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵 ) → 𝐹 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		fnrel	⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
2		df-fn	⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
3		eleq1a	⊢ ( 𝐴 ∈ 𝐵 → ( dom 𝐹 = 𝐴 → dom 𝐹 ∈ 𝐵 ) )
4	3	impcom	⊢ ( ( dom 𝐹 = 𝐴 ∧ 𝐴 ∈ 𝐵 ) → dom 𝐹 ∈ 𝐵 )
5		resfunexg	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵 ) → ( 𝐹 ↾ dom 𝐹 ) ∈ V )
6	4 5	sylan2	⊢ ( ( Fun 𝐹 ∧ ( dom 𝐹 = 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( 𝐹 ↾ dom 𝐹 ) ∈ V )
7	6	anassrs	⊢ ( ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 ↾ dom 𝐹 ) ∈ V )
8	2 7	sylanb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 ↾ dom 𝐹 ) ∈ V )
9		resdm	⊢ ( Rel 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
10	9	eleq1d	⊢ ( Rel 𝐹 → ( ( 𝐹 ↾ dom 𝐹 ) ∈ V ↔ 𝐹 ∈ V ) )
11	10	biimpa	⊢ ( ( Rel 𝐹 ∧ ( 𝐹 ↾ dom 𝐹 ) ∈ V ) → 𝐹 ∈ V )
12	1 8 11	syl2an2r	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵 ) → 𝐹 ∈ V )