Metamath Proof Explorer

Theorem fvmptt

Description: Closed theorem form of fvmpt . (Contributed by Scott Fenton, 21-Feb-2013) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Assertion fvmptt ⊢ ∀ x x = A → B = C ∧ F = x ∈ D ⟼ B ∧ A ∈ D ∧ C ∈ V → F ⁡ A = C

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ∀ x x = A → B = C ∧ F = x ∈ D ⟼ B ∧ A ∈ D ∧ C ∈ V → F = x ∈ D ⟼ B
2 1 fveq1d ⊢ ∀ x x = A → B = C ∧ F = x ∈ D ⟼ B ∧ A ∈ D ∧ C ∈ V → F ⁡ A = x ∈ D ⟼ B ⁡ A
3 risset ⊢ A ∈ D ↔ ∃ x ∈ D x = A
4 elex ⊢ C ∈ V → C ∈ V
5 nfa1 ⊢ Ⅎ x ∀ x x = A → B = C
6 nfv ⊢ Ⅎ x C ∈ V
7 nffvmpt1 ⊢ Ⅎ _ x x ∈ D ⟼ B ⁡ A
8 7 nfeq1 ⊢ Ⅎ x x ∈ D ⟼ B ⁡ A = C
9 6 8 nfim ⊢ Ⅎ x C ∈ V → x ∈ D ⟼ B ⁡ A = C
10 simprl ⊢ x = A ∧ B = C ∧ x ∈ D ∧ C ∈ V → x ∈ D
11 simplr ⊢ x = A ∧ B = C ∧ x ∈ D ∧ C ∈ V → B = C
12 simprr ⊢ x = A ∧ B = C ∧ x ∈ D ∧ C ∈ V → C ∈ V
13 11 12 eqeltrd ⊢ x = A ∧ B = C ∧ x ∈ D ∧ C ∈ V → B ∈ V
14 eqid ⊢ x ∈ D ⟼ B = x ∈ D ⟼ B
15 14 fvmpt2 ⊢ x ∈ D ∧ B ∈ V → x ∈ D ⟼ B ⁡ x = B
16 10 13 15 syl2anc ⊢ x = A ∧ B = C ∧ x ∈ D ∧ C ∈ V → x ∈ D ⟼ B ⁡ x = B
17 simpll ⊢ x = A ∧ B = C ∧ x ∈ D ∧ C ∈ V → x = A
18 17 fveq2d ⊢ x = A ∧ B = C ∧ x ∈ D ∧ C ∈ V → x ∈ D ⟼ B ⁡ x = x ∈ D ⟼ B ⁡ A
19 16 18 11 3eqtr3d ⊢ x = A ∧ B = C ∧ x ∈ D ∧ C ∈ V → x ∈ D ⟼ B ⁡ A = C
20 19 exp43 ⊢ x = A → B = C → x ∈ D → C ∈ V → x ∈ D ⟼ B ⁡ A = C
21 20 a2i ⊢ x = A → B = C → x = A → x ∈ D → C ∈ V → x ∈ D ⟼ B ⁡ A = C
22 21 com23 ⊢ x = A → B = C → x ∈ D → x = A → C ∈ V → x ∈ D ⟼ B ⁡ A = C
23 22 sps ⊢ ∀ x x = A → B = C → x ∈ D → x = A → C ∈ V → x ∈ D ⟼ B ⁡ A = C
24 5 9 23 rexlimd ⊢ ∀ x x = A → B = C → ∃ x ∈ D x = A → C ∈ V → x ∈ D ⟼ B ⁡ A = C
25 4 24 syl7 ⊢ ∀ x x = A → B = C → ∃ x ∈ D x = A → C ∈ V → x ∈ D ⟼ B ⁡ A = C
26 3 25 syl5bi ⊢ ∀ x x = A → B = C → A ∈ D → C ∈ V → x ∈ D ⟼ B ⁡ A = C
27 26 imp32 ⊢ ∀ x x = A → B = C ∧ A ∈ D ∧ C ∈ V → x ∈ D ⟼ B ⁡ A = C
28 27 3adant2 ⊢ ∀ x x = A → B = C ∧ F = x ∈ D ⟼ B ∧ A ∈ D ∧ C ∈ V → x ∈ D ⟼ B ⁡ A = C
29 2 28 eqtrd ⊢ ∀ x x = A → B = C ∧ F = x ∈ D ⟼ B ∧ A ∈ D ∧ C ∈ V → F ⁡ A = C