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 \in V$
	elmap.2	$⊢ B \in V$
Assertion	elpm2	$⊢ F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (F : dom F ⟶ A \land dom F \subseteq B)$

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