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 ) )