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

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 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