This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elpmi

Description: A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015)

Ref Expression
Assertion elpmi 
|- ( F e. ( A ^pm B ) -> ( F : dom F --> A /\ dom F C_ B ) )

Proof

Step Hyp Ref Expression
1 n0i 
 |-  ( F e. ( A ^pm B ) -> -. ( A ^pm B ) = (/) )
2 fnpm 
 |-  ^pm Fn ( _V X. _V )
3 2 fndmi 
 |-  dom ^pm = ( _V X. _V )
4 3 ndmov 
 |-  ( -. ( A e. _V /\ B e. _V ) -> ( A ^pm B ) = (/) )
5 1 4 nsyl2 
 |-  ( F e. ( A ^pm B ) -> ( A e. _V /\ B e. _V ) )
6 elpm2g 
 |-  ( ( A e. _V /\ B e. _V ) -> ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) ) )
7 5 6 syl 
 |-  ( F e. ( A ^pm B ) -> ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) ) )
8 7 ibi 
 |-  ( F e. ( A ^pm B ) -> ( F : dom F --> A /\ dom F C_ B ) )