Theorem dmmptg

Description: The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013) (Revised by Mario Carneiro, 14-Sep-2013)

	Ref	Expression
Assertion	dmmptg	|- ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
2	1	dmmpt	|- dom ( x e. A |-> B ) = { x e. A | B e. _V }
3		elex	|- ( B e. V -> B e. _V )
4	3	ralimi	|- ( A. x e. A B e. V -> A. x e. A B e. _V )
5		rabid2	|- ( A = { x e. A | B e. _V } <-> A. x e. A B e. _V )
6	4 5	sylibr	|- ( A. x e. A B e. V -> A = { x e. A | B e. _V } )
7	2 6	eqtr4id	|- ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )