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 e. _V
	mptexw.2	|- C e. _V
	mptexw.3	|- A. x e. A B e. C
Assertion	mptexw	|- ( x e. A |-> B ) e. _V

Proof

Step	Hyp	Ref	Expression
1		mptexw.1	|- A e. _V
2		mptexw.2	|- C e. _V
3		mptexw.3	|- A. x e. A B e. C
4		funmpt	|- Fun ( x e. A |-> B )
5		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
6	5	dmmptss	|- dom ( x e. A |-> B ) C_ A
7	1 6	ssexi	|- dom ( x e. A |-> B ) e. _V
8	5	rnmptss	|- ( A. x e. A B e. C -> ran ( x e. A |-> B ) C_ C )
9	3 8	ax-mp	|- ran ( x e. A |-> B ) C_ C
10	2 9	ssexi	|- ran ( x e. A |-> B ) e. _V
11		funexw	|- ( ( Fun ( x e. A |-> B ) /\ dom ( x e. A |-> B ) e. _V /\ ran ( x e. A |-> B ) e. _V ) -> ( x e. A |-> B ) e. _V )
12	4 7 10 11	mp3an	|- ( x e. A |-> B ) e. _V