Theorem fvmptnf

Description: The value of a function given by an ordered-pair class abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvmptn uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	fvmptf.1	|- F/_ x A
	fvmptf.2	|- F/_ x C
	fvmptf.3	|- ( x = A -> B = C )
	fvmptf.4	|- F = ( x e. D |-> B )
Assertion	fvmptnf	|- ( -. C e. _V -> ( F ` A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		fvmptf.1	|- F/_ x A
2		fvmptf.2	|- F/_ x C
3		fvmptf.3	|- ( x = A -> B = C )
4		fvmptf.4	|- F = ( x e. D |-> B )
5	4	dmmptss	|- dom F C_ D
6	5	sseli	|- ( A e. dom F -> A e. D )
7		eqid	|- ( x e. D |-> ( _I ` B ) ) = ( x e. D |-> ( _I ` B ) )
8	4 7	fvmptex	|- ( F ` A ) = ( ( x e. D |-> ( _I ` B ) ) ` A )
9		fvex	|- ( _I ` C ) e. _V
10		nfcv	|- F/_ x _I
11	10 2	nffv	|- F/_ x ( _I ` C )
12	3	fveq2d	|- ( x = A -> ( _I ` B ) = ( _I ` C ) )
13	1 11 12 7	fvmptf	|- ( ( A e. D /\ ( _I ` C ) e. _V ) -> ( ( x e. D |-> ( _I ` B ) ) ` A ) = ( _I ` C ) )
14	9 13	mpan2	|- ( A e. D -> ( ( x e. D |-> ( _I ` B ) ) ` A ) = ( _I ` C ) )
15	8 14	syl5eq	|- ( A e. D -> ( F ` A ) = ( _I ` C ) )
16		fvprc	|- ( -. C e. _V -> ( _I ` C ) = (/) )
17	15 16	sylan9eq	|- ( ( A e. D /\ -. C e. _V ) -> ( F ` A ) = (/) )
18	17	expcom	|- ( -. C e. _V -> ( A e. D -> ( F ` A ) = (/) ) )
19	6 18	syl5	|- ( -. C e. _V -> ( A e. dom F -> ( F ` A ) = (/) ) )
20		ndmfv	|- ( -. A e. dom F -> ( F ` A ) = (/) )
21	19 20	pm2.61d1	|- ( -. C e. _V -> ( F ` A ) = (/) )