pmex

Description: The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007)

		Ref	Expression
	Assertion	pmex	$⊢ (A \in C \land B \in D) \to \{f \| (Fun f \land f \subseteq A \times B)\} \in V$

Step	Hyp	Ref	Expression
1		ancom	$⊢ (Fun f \land f \subseteq A \times B) \leftrightarrow (f \subseteq A \times B \land Fun f)$
2	1	abbii	$⊢ \{f \| (Fun f \land f \subseteq A \times B)\} = \{f \| (f \subseteq A \times B \land Fun f)\}$
3		xpexg	$⊢ (A \in C \land B \in D) \to A \times B \in V$
4		abssexg	$⊢ A \times B \in V \to \{f \| (f \subseteq A \times B \land Fun f)\} \in V$
5	3 4	syl	$⊢ (A \in C \land B \in D) \to \{f \| (f \subseteq A \times B \land Fun f)\} \in V$
6	2 5	eqeltrid	$⊢ (A \in C \land B \in D) \to \{f \| (Fun f \land f \subseteq A \times B)\} \in V$

Metamath Proof Explorer