Metamath Proof Explorer

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 ∈ B → F ∈ 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 ∈ B → dom ⁡ F = A → dom ⁡ F ∈ B
4 3 impcom ⊢ dom ⁡ F = A ∧ A ∈ B → dom ⁡ F ∈ B
5 resfunexg ⊢ Fun ⁡ F ∧ dom ⁡ F ∈ B → F ↾ dom ⁡ F ∈ V
6 4 5 sylan2 ⊢ Fun ⁡ F ∧ dom ⁡ F = A ∧ A ∈ B → F ↾ dom ⁡ F ∈ V
7 6 anassrs ⊢ Fun ⁡ F ∧ dom ⁡ F = A ∧ A ∈ B → F ↾ dom ⁡ F ∈ V
8 2 7 sylanb ⊢ F Fn A ∧ A ∈ B → F ↾ dom ⁡ F ∈ V
9 resdm ⊢ Rel ⁡ F → F ↾ dom ⁡ F = F
10 9 eleq1d ⊢ Rel ⁡ F → F ↾ dom ⁡ F ∈ V ↔ F ∈ V
11 10 biimpa ⊢ Rel ⁡ F ∧ F ↾ dom ⁡ F ∈ V → F ∈ V
12 1 8 11 syl2an2r ⊢ F Fn A ∧ A ∈ B → F ∈ V