Metamath Proof Explorer

Theorem elpm2g

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

		Ref	Expression
	Assertion	elpm2g	$⊢ (A \in V \land B \in W) \to (F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (F : dom F ⟶ A \land dom F \subseteq B))$

Step	Hyp	Ref	Expression
1		elpmg	$⊢ (A \in V \land B \in W) \to (F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (Fun F \land F \subseteq B \times A))$
2		funssxp	$⊢ (Fun F \land F \subseteq B \times A) \leftrightarrow (F : dom F ⟶ A \land dom F \subseteq B)$
3	1 2	bitrdi	$⊢ (A \in V \land B \in W) \to (F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (F : dom F ⟶ A \land dom F \subseteq B))$