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	⊢ Ⅎ 𝑥 𝐴
	fvmptf.2	⊢ Ⅎ 𝑥 𝐶
	fvmptf.3	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
	fvmptf.4	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
Assertion	fvmptnf	⊢ ( ¬ 𝐶 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		fvmptf.1	⊢ Ⅎ 𝑥 𝐴
2		fvmptf.2	⊢ Ⅎ 𝑥 𝐶
3		fvmptf.3	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
4		fvmptf.4	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
5	4	dmmptss	⊢ dom 𝐹 ⊆ 𝐷
6	5	sseli	⊢ ( 𝐴 ∈ dom 𝐹 → 𝐴 ∈ 𝐷 )
7		eqid	⊢ ( 𝑥 ∈ 𝐷 ↦ ( I ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( I ‘ 𝐵 ) )
8	4 7	fvmptex	⊢ ( 𝐹 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝐷 ↦ ( I ‘ 𝐵 ) ) ‘ 𝐴 )
9		fvex	⊢ ( I ‘ 𝐶 ) ∈ V
10		nfcv	⊢ Ⅎ 𝑥 I
11	10 2	nffv	⊢ Ⅎ 𝑥 ( I ‘ 𝐶 )
12	3	fveq2d	⊢ ( 𝑥 = 𝐴 → ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) )
13	1 11 12 7	fvmptf	⊢ ( ( 𝐴 ∈ 𝐷 ∧ ( I ‘ 𝐶 ) ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( I ‘ 𝐵 ) ) ‘ 𝐴 ) = ( I ‘ 𝐶 ) )
14	9 13	mpan2	⊢ ( 𝐴 ∈ 𝐷 → ( ( 𝑥 ∈ 𝐷 ↦ ( I ‘ 𝐵 ) ) ‘ 𝐴 ) = ( I ‘ 𝐶 ) )
15	8 14	syl5eq	⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = ( I ‘ 𝐶 ) )
16		fvprc	⊢ ( ¬ 𝐶 ∈ V → ( I ‘ 𝐶 ) = ∅ )
17	15 16	sylan9eq	⊢ ( ( 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
18	17	expcom	⊢ ( ¬ 𝐶 ∈ V → ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = ∅ ) )
19	6 18	syl5	⊢ ( ¬ 𝐶 ∈ V → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ ) )
20		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
21	19 20	pm2.61d1	⊢ ( ¬ 𝐶 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ )