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 ⊢ Ⅎ _ x A
fvmptf.2 ⊢ Ⅎ _ x C
fvmptf.3 ⊢ x = A → B = C
fvmptf.4 ⊢ F = x ∈ D ⟼ B
Assertion fvmptf ⊢ A ∈ D ∧ C ∈ V → F ⁡ A = C

Proof

Step Hyp Ref Expression
1 fvmptf.1 ⊢ Ⅎ _ x A
2 fvmptf.2 ⊢ Ⅎ _ x C
3 fvmptf.3 ⊢ x = A → B = C
4 fvmptf.4 ⊢ F = x ∈ D ⟼ B
5 2 nfel1 ⊢ Ⅎ x C ∈ V
6 nfmpt1 ⊢ Ⅎ _ x x ∈ D ⟼ B
7 4 6 nfcxfr ⊢ Ⅎ _ x F
8 7 1 nffv ⊢ Ⅎ _ x F ⁡ A
9 8 2 nfeq ⊢ Ⅎ x F ⁡ A = C
10 5 9 nfim ⊢ Ⅎ x C ∈ V → F ⁡ A = C
11 3 eleq1d ⊢ x = A → B ∈ V ↔ C ∈ V
12 fveq2 ⊢ x = A → F ⁡ x = F ⁡ A
13 12 3 eqeq12d ⊢ x = A → F ⁡ x = B ↔ F ⁡ A = C
14 11 13 imbi12d ⊢ x = A → B ∈ V → F ⁡ x = B ↔ C ∈ V → F ⁡ A = C
15 4 fvmpt2 ⊢ x ∈ D ∧ B ∈ V → F ⁡ x = B
16 15 ex ⊢ x ∈ D → B ∈ V → F ⁡ x = B
17 1 10 14 16 vtoclgaf ⊢ A ∈ D → C ∈ V → F ⁡ A = C
18 elex ⊢ C ∈ V → C ∈ V
19 17 18 impel ⊢ A ∈ D ∧ C ∈ V → F ⁡ A = C