Metamath Proof Explorer


Theorem elpm2

Description: The predicate "is a partial function." (Contributed by NM, 15-Nov-2007) (Revised by Mario Carneiro, 31-Dec-2013)

Ref Expression
Hypotheses elmap.1
|- A e. _V
elmap.2
|- B e. _V
Assertion elpm2
|- ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) )

Proof

Step Hyp Ref Expression
1 elmap.1
 |-  A e. _V
2 elmap.2
 |-  B e. _V
3 elpm2g
 |-  ( ( A e. _V /\ B e. _V ) -> ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) ) )
4 1 2 3 mp2an
 |-  ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) )