This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )