Metamath Proof Explorer

Theorem mptexgf

Description: If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011) (Revised by Mario Carneiro, 31-Aug-2015) (Revised by Thierry Arnoux, 17-May-2020)

		Ref	Expression
	Hypothesis	mptexgf.a	$⊢ \underline{Ⅎ} x A$
	Assertion	mptexgf	$⊢ A \in V \to (x \in A ⟼ B) \in V$

Proof

Step	Hyp	Ref	Expression
1		mptexgf.a	$⊢ \underline{Ⅎ} x A$
2		funmpt	$⊢ Fun (x \in A ⟼ B)$
3		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
4	3	dmmpt	$⊢ dom (x \in A ⟼ B) = \{x \in A \| B \in V\}$
5		tru	$⊢ ⊤$
6	5	2a1i	$⊢ x \in A \to (B \in V \to ⊤)$
7	6	ss2rabi	$⊢ \{x \in A \| B \in V\} \subseteq \{x \in A \| ⊤\}$
8	1	rabtru	$⊢ \{x \in A \| ⊤\} = A$
9	7 8	sseqtri	$⊢ \{x \in A \| B \in V\} \subseteq A$
10	4 9	eqsstri	$⊢ dom (x \in A ⟼ B) \subseteq A$
11		ssexg	$⊢ (dom (x \in A ⟼ B) \subseteq A \land A \in V) \to dom (x \in A ⟼ B) \in V$
12	10 11	mpan	$⊢ A \in V \to dom (x \in A ⟼ B) \in V$
13		funex	$⊢ (Fun (x \in A ⟼ B) \land dom (x \in A ⟼ B) \in V) \to (x \in A ⟼ B) \in V$
14	2 12 13	sylancr	$⊢ A \in V \to (x \in A ⟼ B) \in V$