Metamath Proof Explorer

Theorem mptexw

Description: Weak version of mptex that holds without ax-rep . If the domain and codomain of a function given by maps-to notation are sets, the function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023)

		Ref	Expression
	Hypotheses	mptexw.1	$⊢ A \in V$
		mptexw.2	$⊢ C \in V$
		mptexw.3	$⊢ \forall x \in A B \in C$
	Assertion	mptexw	$⊢ (x \in A ⟼ B) \in V$

Proof

Step	Hyp	Ref	Expression
1		mptexw.1	$⊢ A \in V$
2		mptexw.2	$⊢ C \in V$
3		mptexw.3	$⊢ \forall x \in A B \in C$
4		funmpt	$⊢ Fun (x \in A ⟼ B)$
5		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
6	5	dmmptss	$⊢ dom (x \in A ⟼ B) \subseteq A$
7	1 6	ssexi	$⊢ dom (x \in A ⟼ B) \in V$
8	5	rnmptss	$⊢ \forall x \in A B \in C \to ran (x \in A ⟼ B) \subseteq C$
9	3 8	ax-mp	$⊢ ran (x \in A ⟼ B) \subseteq C$
10	2 9	ssexi	$⊢ ran (x \in A ⟼ B) \in V$
11		funexw	$⊢ (Fun (x \in A ⟼ B) \land dom (x \in A ⟼ B) \in V \land ran (x \in A ⟼ B) \in V) \to (x \in A ⟼ B) \in V$
12	4 7 10 11	mp3an	$⊢ (x \in A ⟼ B) \in V$