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

Metamath Proof Explorer

Theorem fvmptdv2

Description: Alternate deduction version of fvmpt , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017)

Ref Expression
Hypotheses fvmptdv2.1 ⊢ φ → A ∈ D
fvmptdv2.2 ⊢ φ ∧ x = A → B ∈ V
fvmptdv2.3 ⊢ φ ∧ x = A → B = C
Assertion fvmptdv2 ⊢ φ → F = x ∈ D ⟼ B → F ⁡ A = C

Proof

Step Hyp Ref Expression
1 fvmptdv2.1 ⊢ φ → A ∈ D
2 fvmptdv2.2 ⊢ φ ∧ x = A → B ∈ V
3 fvmptdv2.3 ⊢ φ ∧ x = A → B = C
4 eqidd ⊢ φ → x ∈ D ⟼ B = x ∈ D ⟼ B
5 1 elexd ⊢ φ → A ∈ V
6 isset ⊢ A ∈ V ↔ ∃ x x = A
7 5 6 sylib ⊢ φ → ∃ x x = A
8 2 elexd ⊢ φ ∧ x = A → B ∈ V
9 3 8 eqeltrrd ⊢ φ ∧ x = A → C ∈ V
10 7 9 exlimddv ⊢ φ → C ∈ V
11 4 3 1 10 fvmptd ⊢ φ → x ∈ D ⟼ B ⁡ A = C
12 fveq1 ⊢ F = x ∈ D ⟼ B → F ⁡ A = x ∈ D ⟼ B ⁡ A
13 12 eqeq1d ⊢ F = x ∈ D ⟼ B → F ⁡ A = C ↔ x ∈ D ⟼ B ⁡ A = C
14 11 13 syl5ibrcom ⊢ φ → F = x ∈ D ⟼ B → F ⁡ A = C