Metamath Proof Explorer


Theorem fabex

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

Ref Expression
Hypotheses fabex.1
|- A e. _V
fabex.2
|- B e. _V
fabex.3
|- F = { x | ( x : A --> B /\ ph ) }
Assertion fabex
|- F e. _V

Proof

Step Hyp Ref Expression
1 fabex.1
 |-  A e. _V
2 fabex.2
 |-  B e. _V
3 fabex.3
 |-  F = { x | ( x : A --> B /\ ph ) }
4 3 fabexg
 |-  ( ( A e. _V /\ B e. _V ) -> F e. _V )
5 1 2 4 mp2an
 |-  F e. _V