This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mptexg

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)

		Ref	Expression
	Assertion	mptexg	$⊢ A \in V \to (x \in A ⟼ B) \in V$

Proof

Step	Hyp	Ref	Expression
1		funmpt	$⊢ Fun (x \in A ⟼ B)$
2		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
3	2	dmmptss	$⊢ dom (x \in A ⟼ B) \subseteq A$
4		ssexg	$⊢ (dom (x \in A ⟼ B) \subseteq A \land A \in V) \to dom (x \in A ⟼ B) \in V$
5	3 4	mpan	$⊢ A \in V \to dom (x \in A ⟼ B) \in V$
6		funex	$⊢ (Fun (x \in A ⟼ B) \land dom (x \in A ⟼ B) \in V) \to (x \in A ⟼ B) \in V$
7	1 5 6	sylancr	$⊢ A \in V \to (x \in A ⟼ B) \in V$