Theorem mpt0

Description: A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Assertion	mpt0	|- ( x e. (/) |-> A ) = (/)

Proof

Step	Hyp	Ref	Expression
1		ral0	|- A. x e. (/) A e. _V
2		eqid	|- ( x e. (/) |-> A ) = ( x e. (/) |-> A )
3	2	fnmpt	|- ( A. x e. (/) A e. _V -> ( x e. (/) |-> A ) Fn (/) )
4	1 3	ax-mp	|- ( x e. (/) |-> A ) Fn (/)
5		fn0	|- ( ( x e. (/) |-> A ) Fn (/) <-> ( x e. (/) |-> A ) = (/) )
6	4 5	mpbi	|- ( x e. (/) |-> A ) = (/)