Metamath Proof Explorer

Theorem elpm

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

	Ref	Expression
Hypotheses	elmap.1	$⊢ A \in V$
	elmap.2	$⊢ B \in V$
Assertion	elpm	$⊢ F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (Fun F \land F \subseteq B \times A)$

Step	Hyp	Ref	Expression
1		elmap.1	$⊢ A \in V$
2		elmap.2	$⊢ B \in V$
3		elpmg	$⊢ (A \in V \land B \in V) \to (F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (Fun F \land F \subseteq B \times A))$
4	1 2 3	mp2an	$⊢ F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (Fun F \land F \subseteq B \times A)$