Theorem fabex

Description: Existence of a set of functions. (Contributed by NM, 3-Dec-2007)

	Ref	Expression
Hypotheses	fabex.1	⊢ 𝐴 ∈ V
	fabex.2	⊢ 𝐵 ∈ V
	fabex.3	⊢ 𝐹 = { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) }
Assertion	fabex	⊢ 𝐹 ∈ V

Proof

Step	Hyp	Ref	Expression
1		fabex.1	⊢ 𝐴 ∈ V
2		fabex.2	⊢ 𝐵 ∈ V
3		fabex.3	⊢ 𝐹 = { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) }
4	3	fabexg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐹 ∈ V )
5	1 2 4	mp2an	⊢ 𝐹 ∈ V