Theorem fvmptf

Description: Value of a function given by an ordered-pair class abstraction. This version of fvmptg uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	fvmptf.1	⊢ Ⅎ 𝑥 𝐴
	fvmptf.2	⊢ Ⅎ 𝑥 𝐶
	fvmptf.3	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
	fvmptf.4	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
Assertion	fvmptf	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvmptf.1	⊢ Ⅎ 𝑥 𝐴
2		fvmptf.2	⊢ Ⅎ 𝑥 𝐶
3		fvmptf.3	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
4		fvmptf.4	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
5	2	nfel1	⊢ Ⅎ 𝑥 𝐶 ∈ V
6		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
7	4 6	nfcxfr	⊢ Ⅎ 𝑥 𝐹
8	7 1	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝐴 )
9	8 2	nfeq	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝐴 ) = 𝐶
10	5 9	nfim	⊢ Ⅎ 𝑥 ( 𝐶 ∈ V → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
11	3	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∈ V ↔ 𝐶 ∈ V ) )
12		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
13	12 3	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = 𝐵 ↔ ( 𝐹 ‘ 𝐴 ) = 𝐶 ) )
14	11 13	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ∈ V → ( 𝐹 ‘ 𝑥 ) = 𝐵 ) ↔ ( 𝐶 ∈ V → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) ) )
15	4	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝐵 ∈ V ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
16	15	ex	⊢ ( 𝑥 ∈ 𝐷 → ( 𝐵 ∈ V → ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
17	1 10 14 16	vtoclgaf	⊢ ( 𝐴 ∈ 𝐷 → ( 𝐶 ∈ V → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) )
18		elex	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ V )
19	17 18	impel	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )