Metamath Proof Explorer

Theorem elpm2g

Description: The predicate "is a partial function." (Contributed by NM, 31-Dec-2013)

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

Step	Hyp	Ref	Expression
1		elpmg	\|- ( ( A e. V /\ B e. W ) -> ( F e. ( A ^pm B ) <-> ( Fun F /\ F C_ ( B X. A ) ) ) )
2		funssxp	\|- ( ( Fun F /\ F C_ ( B X. A ) ) <-> ( F : dom F --> A /\ dom F C_ B ) )
3	1 2	bitrdi	\|- ( ( A e. V /\ B e. W ) -> ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) ) )

Step

Hyp

Ref

Expression

 |-  ( ( A e. V /\ B e. W ) -> ( F e. ( A ^pm B ) <-> ( Fun F /\ F C_ ( B X. A ) ) ) )

 |-  ( ( Fun F /\ F C_ ( B X. A ) ) <-> ( F : dom F --> A /\ dom F C_ B ) )

1 2

 |-  ( ( A e. V /\ B e. W ) -> ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) ) )